diff --git a/README.md b/README.md index c34818de..74ba60de 100644 --- a/README.md +++ b/README.md @@ -57,8 +57,16 @@ selfie -c -o To display the available subcommands that Unicorn has you can type `./target/debug/unicorn --help`, or to display subcommand options `./target/debug/unicorn --help`. -Currently, there are 3 main commands: -### 1. Generate a BTOR2 file from a binary +We give a short tutorial for 3 commands in the following sections: + +
    +
  1. beator to generate BTOR2 files.
    2. +
  2. quarc to generate quantum circuits.
    3. +
  3. qubot to generate QUBO/ISING models.
    4. +
+ +

1. Generate a BTOR2 file from a binary

+ ```sh ./target/debug/unicorn beator --unroll --solver boolector --out ``` @@ -66,8 +74,42 @@ The above command generates a BTOR2 file, while the unroll option specifies how There are more options. For example, you can add `--bitblast` to the command, and the BTOR2 file will represent a logic (combinatorial) circuit. +

2. Quantum Circuits with QUARC

+QUARC builds quantum circuits, more concretely it builds oracles for Grover's algorithm. You can build and test a quantum circuit: + +```sh +target/debug/unicorn quarc --unroll --solver --inputs +``` + +Which for example can be + +```sh +target/debug/unicorn quarc examples/selfie/d.m --unroll 84 --inputs 42-49-0 +``` + +The above command will unroll the finite state machine of the program `d.m` 84 times, and it will execute inputs 42, 49 and 0 in the oracle. The output is the following: + +``` +******* QUANTUM CIRCUIT STATS ******** +Qubits required: 384 +Total gates: 2968 +Single-qubit gates: 343 +MCX gates: 2625 +Max. controls in MCX: 18 +************************************** +[42] evaluates to true + +[49] evaluates to true + +[0] evaluates to false +``` +Meaning that inputs `42` and `49` makes the oracle evaluate to `true`, while input `0` makes de oracle evaluate to `false`. + +A Python binding is coming soon! + +

3. QUBOT

+Similarly, QUBOT can also build and test its models. -### 2. Generate and/or test a QUBO of the binary ```sh ./target/debug/unicorn qubot --unroll --solver --out --inputs 42,32;34 ``` diff --git a/examples/quarc/add.btor2 b/examples/quarc/add.btor2 new file mode 100644 index 00000000..c4f29a19 --- /dev/null +++ b/examples/quarc/add.btor2 @@ -0,0 +1,10 @@ +1 sort bitvec 8 +2 input 1 +3 input 1 +4 state 1 +9 constd 1 0 +10 init 1 4 9 +5 add 1 2 3 +6 next 1 4 5 +7 eq 1 4 4 +8 bad 7 diff --git a/examples/quarc/add2.btor2 b/examples/quarc/add2.btor2 new file mode 100644 index 00000000..8e2bbd2b --- /dev/null +++ b/examples/quarc/add2.btor2 @@ -0,0 +1,9 @@ +1 sort bitvec 8 +2 input 1 +4 state 1 +9 constd 1 10 +10 init 1 4 9 +5 add 1 4 2 +6 next 1 4 5 +7 eq 1 4 4 +8 bad 7 diff --git a/examples/quarc/and.btor2 b/examples/quarc/and.btor2 new file mode 100644 index 00000000..d2d2fc0f --- /dev/null +++ b/examples/quarc/and.btor2 @@ -0,0 +1,10 @@ +1 sort bitvec 8 +2 input 1 +3 input 1 +4 state 1 +9 constd 1 0 +10 init 1 4 9 +5 and 1 2 3 +6 next 1 4 5 +7 eq 1 4 4 +8 bad 7 diff --git a/examples/quarc/and2.btor2 b/examples/quarc/and2.btor2 new file mode 100644 index 00000000..fbfc5530 --- /dev/null +++ b/examples/quarc/and2.btor2 @@ -0,0 +1,9 @@ +1 sort bitvec 8 +2 input 1 +4 state 1 +9 constd 1 241 +10 init 1 4 9 +5 and 1 4 2 +6 next 1 4 5 +7 eq 1 4 4 +8 bad 7 diff --git a/examples/quarc/div.btor2 b/examples/quarc/div.btor2 new file mode 100644 index 00000000..c8d1a4fc --- /dev/null +++ b/examples/quarc/div.btor2 @@ -0,0 +1,10 @@ +1 sort bitvec 8 +2 input 1 +3 input 1 +4 state 1 +9 constd 1 0 +10 init 1 4 9 +5 udiv 1 2 3 +6 next 1 4 5 +7 eq 1 4 4 +8 bad 7 diff --git a/examples/quarc/div2.btor2 b/examples/quarc/div2.btor2 new file mode 100644 index 00000000..f401545a --- /dev/null +++ b/examples/quarc/div2.btor2 @@ -0,0 +1,9 @@ +1 sort bitvec 8 +2 input 1 +4 state 1 +9 constd 1 50 +10 init 1 4 9 +5 udiv 1 2 4 +6 next 1 4 5 +7 eq 1 4 4 +8 bad 7 diff --git a/examples/quarc/eq.btor2 b/examples/quarc/eq.btor2 new file mode 100644 index 00000000..885cbec8 --- /dev/null +++ b/examples/quarc/eq.btor2 @@ -0,0 +1,5 @@ +1 sort bitvec 1 +2 input 1 +3 input 1 +4 eq 1 2 3 +5 bad 4 diff --git a/examples/quarc/eq8.btor2 b/examples/quarc/eq8.btor2 new file mode 100644 index 00000000..a9f436bf --- /dev/null +++ b/examples/quarc/eq8.btor2 @@ -0,0 +1,5 @@ +1 sort bitvec 8 +2 input 1 +3 input 1 +4 eq 1 2 3 +5 bad 4 diff --git a/examples/quarc/eq82.btor2 b/examples/quarc/eq82.btor2 new file mode 100644 index 00000000..58553c21 --- /dev/null +++ b/examples/quarc/eq82.btor2 @@ -0,0 +1,7 @@ +1 sort bitvec 8 +2 input 1 +3 state 1 +9 constd 1 0 +10 init 1 3 9 +4 eq 1 2 3 +5 bad 4 diff --git a/examples/quarc/ite.btor2 b/examples/quarc/ite.btor2 new file mode 100644 index 00000000..bd39b0c2 --- /dev/null +++ b/examples/quarc/ite.btor2 @@ -0,0 +1,11 @@ +1 sort bitvec 1 +2 sort bitvec 8 +3 input 1 +4 input 2 +5 input 2 +6 ite 1 3 4 5 +10 state 2 +11 constd 1 241 +12 init 1 10 11 +7 next 1 10 6 +9 bad 3 diff --git a/examples/quarc/ite2.btor2 b/examples/quarc/ite2.btor2 new file mode 100644 index 00000000..333fd231 --- /dev/null +++ b/examples/quarc/ite2.btor2 @@ -0,0 +1,10 @@ +1 sort bitvec 1 +2 sort bitvec 8 +3 input 1 +4 state 2 +11 constd 2 0 +12 init 2 4 11 +5 input 2 +6 ite 1 3 5 4 +7 next 1 4 6 +9 bad 3 diff --git a/examples/quarc/mul.btor2 b/examples/quarc/mul.btor2 new file mode 100644 index 00000000..78b9a550 --- /dev/null +++ b/examples/quarc/mul.btor2 @@ -0,0 +1,10 @@ +1 sort bitvec 8 +2 input 1 +3 input 1 +4 state 1 +9 constd 1 0 +10 init 1 4 9 +5 mul 1 2 3 +6 next 1 4 5 +7 eq 1 4 4 +8 bad 7 diff --git a/examples/quarc/mul2.btor2 b/examples/quarc/mul2.btor2 new file mode 100644 index 00000000..0003ca25 --- /dev/null +++ b/examples/quarc/mul2.btor2 @@ -0,0 +1,9 @@ +1 sort bitvec 8 +2 input 1 +4 state 1 +9 constd 1 3 +10 init 1 4 9 +5 mul 1 2 4 +6 next 1 4 5 +7 eq 1 4 4 +8 bad 7 diff --git a/examples/quarc/not.btor2 b/examples/quarc/not.btor2 new file mode 100644 index 00000000..c8ba5260 --- /dev/null +++ b/examples/quarc/not.btor2 @@ -0,0 +1,6 @@ +1 sort bitvec 8 +3 input 1 +4 not 1 3 +5 next 1 3 4 +7 eq 1 3 3 +8 bad 7 diff --git a/examples/quarc/rem.btor2 b/examples/quarc/rem.btor2 new file mode 100644 index 00000000..a3770bed --- /dev/null +++ b/examples/quarc/rem.btor2 @@ -0,0 +1,10 @@ +1 sort bitvec 8 +2 input 1 +3 input 1 +4 state 1 +9 constd 1 0 +10 init 1 4 9 +5 urem 1 2 3 +6 next 1 4 5 +7 eq 1 4 4 +8 bad 7 diff --git a/examples/quarc/sub.btor2 b/examples/quarc/sub.btor2 new file mode 100644 index 00000000..14822103 --- /dev/null +++ b/examples/quarc/sub.btor2 @@ -0,0 +1,10 @@ +1 sort bitvec 8 +2 input 1 +3 input 1 +4 state 1 +9 constd 1 0 +10 init 1 4 9 +5 sub 1 2 3 +6 next 1 4 5 +7 eq 1 4 4 +8 bad 7 diff --git a/examples/quarc/sub2.btor2 b/examples/quarc/sub2.btor2 new file mode 100644 index 00000000..0fd77835 --- /dev/null +++ b/examples/quarc/sub2.btor2 @@ -0,0 +1,7 @@ +1 sort bitvec 8 +2 input 1 +4 state 1 +9 constd 1 255 +10 init 1 4 9 +5 sub 1 4 2 +6 next 1 4 5 diff --git a/examples/quarc/ult.btor2 b/examples/quarc/ult.btor2 new file mode 100644 index 00000000..32ff8b8b --- /dev/null +++ b/examples/quarc/ult.btor2 @@ -0,0 +1,5 @@ +1 sort bitvec 8 +2 input 1 +3 input 1 +4 ult 1 2 3 +5 bad 4 diff --git a/examples/quarc/ult2.btor2 b/examples/quarc/ult2.btor2 new file mode 100644 index 00000000..7557b149 --- /dev/null +++ b/examples/quarc/ult2.btor2 @@ -0,0 +1,7 @@ +1 sort bitvec 8 +2 input 1 +3 state 1 +9 constd 1 213 +10 init 1 3 9 +4 ult 1 2 3 +5 bad 4 diff --git a/examples/selfie/d.c b/examples/selfie/d.c new file mode 100644 index 00000000..df04ac8d --- /dev/null +++ b/examples/selfie/d.c @@ -0,0 +1,10 @@ +uint64_t* x; +uint64_t main() { uint64_t a; + x = malloc(1); // rounded up to 8 + // touch to trigger page fault here + *x = 0; + // read 1 byte from console into x + read(0, x, 1); + a = *x; + a = *(x + a); // segfault if input != 0 +} \ No newline at end of file diff --git a/examples/selfie/d.m b/examples/selfie/d.m new file mode 100755 index 00000000..46b0775b Binary files /dev/null and b/examples/selfie/d.m differ diff --git a/examples/selfie/division-by-zero-3-35.c b/examples/selfie/division-by-zero-3-35.c new file mode 100644 index 00000000..8eef6ddb --- /dev/null +++ b/examples/selfie/division-by-zero-3-35.c @@ -0,0 +1,25 @@ +uint64_t main() { + uint64_t a; + uint64_t* x; + + x = malloc(8); + + *x = 0; // touch memory + + read(0, x, 1); + + *x = *x - 48; + + // division by zero if the input is '0' (== 48 == b00110000) + a = 41 + (1 / *x); + + // division by zero if the input is '2' (== 50 == b00110010) + if (*x == 2) + a = 41 + (1 / 0); + + if (a == 42) + // non-zero exit code if the input is '1' (== 49 == b00110001) + return 1; + else + return 0; +} diff --git a/examples/selfie/division-by-zero-3-35.m b/examples/selfie/division-by-zero-3-35.m new file mode 100755 index 00000000..11cf1e9f Binary files /dev/null and b/examples/selfie/division-by-zero-3-35.m differ diff --git a/examples/selfie/memory-access-fail-1-35.c b/examples/selfie/memory-access-fail-1-35.c new file mode 100644 index 00000000..c25965df --- /dev/null +++ b/examples/selfie/memory-access-fail-1-35.c @@ -0,0 +1,59 @@ +uint64_t main() { + uint64_t* x; + uint64_t* v; + + x = malloc(8); + + *x = 0; // touch memory + + // access code segment by reaching over data segment with _bump variable, no --check-block-access required + + v = x + -(4096 / 8) + -1; + + *v = *v; + open(v, 32768, 0); + read(0, v, 1); + write(1, v, 1); + + // access memory right above 4GB, avoiding big integer in data segment, no --check-block-access required + + v = x + ((uint64_t*) (4 * 1024 * 1024 * 1024) - x); + + *v = *v; + open(v, 32768, 0); + read(0, v, 1); + write(1, v, 1); + + // access word-unaligned address, no --check-block-access required + + v = (uint64_t*) ((uint64_t) x + 1); + + *v = *v; + open(v, 32768, 0); + read(0, v, 1); + write(1, v, 1); + + // access memory right above memory block but well below 4GB, requires --check-block-access + + v = x + 1; + + *v = *v; + open(v, 32768, 0); + read(0, v, 1); + write(1, v, 1); + + // unsafe access right above memory block even without pointer arithmetic + read(0, x, 9); + write(1, x, 9); + + // access memory right below memory block but still above code segment, due to _bump variable, requires --check-block-access + + v = x + -1; + + *v = *v; + open(v, 32768, 0); + read(0, v, 1); + write(1, v, 1); + + return 0; +} diff --git a/examples/selfie/memory-access-fail-1-35.m b/examples/selfie/memory-access-fail-1-35.m new file mode 100755 index 00000000..e887b7d6 Binary files /dev/null and b/examples/selfie/memory-access-fail-1-35.m differ diff --git a/examples/selfie/nested-if-else-1-35.c b/examples/selfie/nested-if-else-1-35.c new file mode 100644 index 00000000..7d6194a1 --- /dev/null +++ b/examples/selfie/nested-if-else-1-35.c @@ -0,0 +1,27 @@ +uint64_t main() { + uint64_t a; + uint64_t* x; + + a = 40; + x = malloc(8); + + *x = 0; // touch memory + + read(0, x, 1); + + if (*x > 48) { + *x = *x - 47; + + if (*x == 2) + a = a + *x; + else + a = a + (*x * 0); + } else + a = a + (*x * 0); + + if (a == 42) + // non-zero exit code if the input is '1' (== 49 == b00110001) + return 1; + else + return 0; +} diff --git a/examples/selfie/nested-if-else-1-35.m b/examples/selfie/nested-if-else-1-35.m new file mode 100755 index 00000000..c1b3fa7b Binary files /dev/null and b/examples/selfie/nested-if-else-1-35.m differ diff --git a/examples/selfie/nested-if-else-reverse-1-35.c b/examples/selfie/nested-if-else-reverse-1-35.c new file mode 100644 index 00000000..3bd2bcd7 --- /dev/null +++ b/examples/selfie/nested-if-else-reverse-1-35.c @@ -0,0 +1,28 @@ +uint64_t main() { + uint64_t a; + uint64_t* x; + + a = 40; + x = malloc(8); + + *x = 0; // touch memory + + read(0, x, 1); + + if (*x <= 48) + a = a + (*x * 0); + else { + *x = *x - 47; + + if (*x != 2) + a = a + (*x * 0); + else + a = a + *x; + } + + if (a == 42) + // non-zero exit code if the input is '1' (== 49 == b00110001) + return 1; + else + return 0; +} diff --git a/examples/selfie/nested-if-else-reverse-1-35.m b/examples/selfie/nested-if-else-reverse-1-35.m new file mode 100755 index 00000000..980bacf2 Binary files /dev/null and b/examples/selfie/nested-if-else-reverse-1-35.m differ diff --git a/examples/selfie/return-from-loop-1-35.c b/examples/selfie/return-from-loop-1-35.c new file mode 100644 index 00000000..647432e0 --- /dev/null +++ b/examples/selfie/return-from-loop-1-35.c @@ -0,0 +1,23 @@ +uint64_t main() { + uint64_t a; + uint64_t* x; + + x = malloc(8); + + *x = 0; // touch memory + + read(0, x, 1); + + a = 0; + + while (a < 10) { + + // non-zero exit code if the input is a digit + if (*x - 48 == a) + return 1; + + a = a + 1; + } + + return 0; +} diff --git a/examples/selfie/return-from-loop-1-35.m b/examples/selfie/return-from-loop-1-35.m new file mode 100755 index 00000000..693b0843 Binary files /dev/null and b/examples/selfie/return-from-loop-1-35.m differ diff --git a/examples/selfie/simple-assignment-1-35.c b/examples/selfie/simple-assignment-1-35.c new file mode 100644 index 00000000..f45e54ed --- /dev/null +++ b/examples/selfie/simple-assignment-1-35.c @@ -0,0 +1,20 @@ +uint64_t main() { + uint64_t* x; + + x = malloc(8); + + *x = 0; // touch memory + + read(0, x, 1); + + *x = *x - 6; + + if (*x > 42) + // non-zero exit code if the input is > '0' (== 48 == b00110000) + return 1; + else if (*x < 42) + // non-zero exit code if the input is < '0' (== 48 == b00110000) + return 1; + else + return 0; +} diff --git a/examples/selfie/simple-assignment-1-35.m b/examples/selfie/simple-assignment-1-35.m new file mode 100755 index 00000000..a7afbdd5 Binary files /dev/null and b/examples/selfie/simple-assignment-1-35.m differ diff --git a/examples/selfie/simple-if-else-1-35.c b/examples/selfie/simple-if-else-1-35.c new file mode 100644 index 00000000..88b0a7b4 --- /dev/null +++ b/examples/selfie/simple-if-else-1-35.c @@ -0,0 +1,24 @@ +uint64_t main() { + uint64_t a; + uint64_t* x; + + a = 40; + x = malloc(8); + + *x = 0; // touch memory + + read(0, x, 1); + + *x = *x - 47; + + if (*x == 2) + a = a + *x; + else + a = a + (*x * 0); + + if (a == 42) + // non-zero exit code if the input is '1' (== 49 == b00110001) + return 1; + else + return 0; +} diff --git a/examples/selfie/simple-if-else-1-35.m b/examples/selfie/simple-if-else-1-35.m new file mode 100755 index 00000000..33b06597 Binary files /dev/null and b/examples/selfie/simple-if-else-1-35.m differ diff --git a/examples/selfie/simple-if-else-reverse-1-35.c b/examples/selfie/simple-if-else-reverse-1-35.c new file mode 100644 index 00000000..9ed6a277 --- /dev/null +++ b/examples/selfie/simple-if-else-reverse-1-35.c @@ -0,0 +1,24 @@ +uint64_t main() { + uint64_t a; + uint64_t* x; + + a = 40; + x = malloc(8); + + *x = 0; // touch memory + + read(0, x, 1); + + *x = *x - 47; + + if (*x != 2) + a = a + (*x * 0); + else + a = a + *x; + + if (a == 42) + // non-zero exit code if the input is '1' (== 49 == b00110001) + return 1; + else + return 0; +} diff --git a/examples/selfie/simple-if-else-reverse-1-35.m b/examples/selfie/simple-if-else-reverse-1-35.m new file mode 100755 index 00000000..e59a876e Binary files /dev/null and b/examples/selfie/simple-if-else-reverse-1-35.m differ diff --git a/examples/selfie/simple-if-without-else-1-35.c b/examples/selfie/simple-if-without-else-1-35.c new file mode 100644 index 00000000..3d740d27 --- /dev/null +++ b/examples/selfie/simple-if-without-else-1-35.c @@ -0,0 +1,22 @@ +uint64_t main() { + uint64_t a; + uint64_t* x; + + a = 40; + x = malloc(8); + + *x = 0; // touch memory + + read(0, x, 1); + + *x = *x - 47; + + if (*x == 2) + a = a + *x; + + if (a == 42) + // non-zero exit code if the input is '1' (== 49 == b00110001) + return 1; + else + return 0; +} diff --git a/examples/selfie/simple-if-without-else-1-35.m b/examples/selfie/simple-if-without-else-1-35.m new file mode 100755 index 00000000..875371e7 Binary files /dev/null and b/examples/selfie/simple-if-without-else-1-35.m differ diff --git a/src/cli.rs b/src/cli.rs index 0438d44b..f070c0a0 100644 --- a/src/cli.rs +++ b/src/cli.rs @@ -259,6 +259,111 @@ pub fn args() -> Command { .num_args(1..) ) ) + .subcommand( + Command::new("quarc") + .about("Generate quantum circuits from a RISC-U ELF binary file ") + .arg( + Arg::new("input-file") + .help("If --from-btor2 flag is not passed, then RISC-V ELF binary to be converted, else a BTOR2 file.") + .num_args(1) + .value_name("FILE") + .required(true), + ) + .arg( + Arg::new("sat-solver") + .help("SAT solver used for bad-state reasoning") + .long("sat-solver") + .num_args(1) + .value_name("SOLVER") + .value_parser(value_parser_sat_type()) + .default_value(Into::<&str>::into(SatType::None)), + ) + .arg( + Arg::new("dynamic-memory") + .help("Pass this flag to compile a program with dynamic quantum memory") + .short('d') + .long("dynamic-memory") + ) + .arg( + Arg::new("from-btor2") + .help("Pass this flag if the input file is a BTOR2 file.") + .short('f') + .long("from-btor2") + ) + .arg( + Arg::new("output-file") + .help("Output path for the generated QUBO model") + .short('o') + .long("out") + .num_args(1) + ) + .arg( + Arg::new("max-heap") + .help("Number of machine-words usable as heap") + .long("max-heap") + .num_args(1) + .value_name("NUMBER") + .default_value(DEFAULT_MAX_HEAP) + .value_parser(value_parser!(u32)), + ) + .arg( + Arg::new("max-stack") + .help("Number of machine-words usable as stack") + .long("max-stack") + .num_args(1) + .value_name("NUMBER") + .default_value(DEFAULT_MAX_STACK) + .value_parser(value_parser!(u32)), + ) + .arg( + Arg::new("memory") + .help("Total size of memory in MiB [possible: 1 .. 1024]") + .long("memory") + .num_args(1) + .value_name("NUMBER") + .default_value(DEFAULT_MEMORY_SIZE) + .value_parser(value_parser_memory_size()), + ) + .arg( + Arg::new("inputs") + .help("Provide inputs to evaluate the model, separate by commas the values for a single instance, and with semicolon for various instances.") + .short('i') + .long("inputs") + .num_args(1) + ) + .arg( + Arg::new("smt-solver") + .help("SMT solver used for optimization") + .short('s') + .long("solver") + .num_args(1) + .value_name("SOLVER") + .value_parser(value_parser_smt_type()) + .default_value(Into::<&str>::into(SmtType::Generic)), + ) + .arg( + Arg::new("unroll-model") + .help("Number of instructions to unroll from model") + .short('u') + .long("unroll") + .num_args(1) + .value_name("NUMBER") + .value_parser(value_parser!(usize)), + ) + .arg( + Arg::new("from-dimacs") + .help("Consume DIMACS instead of RISC-U inputs") + .long("from-dimacs") + ) + .arg( + Arg::new("extras") + .help("Arguments passed to emulated program") + .value_name("ARGUMENTS") + .last(true) + .allow_hyphen_values(true) + .num_args(1..) + ), + ) .subcommand( Command::new("qubot") .about("Create a QUBO model for a RISC-V ELF binary") diff --git a/src/lib.rs b/src/lib.rs index 69c05296..a0194341 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -4,6 +4,7 @@ pub mod util; pub mod disassemble; pub mod emulate; pub mod engine; +pub mod unicorn; use riscu::{load_object_file, Program}; use std::path::Path; diff --git a/src/main.rs b/src/main.rs index e09b2ad0..41f4e85d 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,23 +1,28 @@ mod cli; mod quantum_annealing; -mod unicorn; use crate::quantum_annealing::dwave_api::sample_quantum_annealer; -use crate::unicorn::bitblasting::bitblast_model; -use crate::unicorn::bitblasting_dimacs::write_dimacs_model; -use crate::unicorn::bitblasting_printer::write_btor2_model; -use crate::unicorn::btor2file_parser::parse_btor2_file; -use crate::unicorn::builder::generate_model; -use crate::unicorn::codegen::compile_model_into_program; -use crate::unicorn::dimacs_parser::load_dimacs_as_gatemodel; -use crate::unicorn::emulate_loader::load_model_into_emulator; -use crate::unicorn::memory::replace_memory; -use crate::unicorn::optimize::{optimize_model_with_input, optimize_model_with_solver}; -use crate::unicorn::qubot::{InputEvaluator, Qubot}; -use crate::unicorn::sat_solver::solve_bad_states; -use crate::unicorn::smt_solver::*; -use crate::unicorn::unroller::{prune_model, renumber_model, unroll_model}; -use crate::unicorn::write_model; +use unicorn::unicorn::bitblasting::bitblast_model; +use unicorn::unicorn::bitblasting_dimacs::write_dimacs_model; +use unicorn::unicorn::bitblasting_printer::write_btor2_model; +use unicorn::unicorn::btor2file_parser::parse_btor2_file; +use unicorn::unicorn::builder::generate_model; +use unicorn::unicorn::codegen::compile_model_into_program; +use unicorn::unicorn::dimacs_parser::load_dimacs_as_gatemodel; +use unicorn::unicorn::emulate_loader::load_model_into_emulator; +use unicorn::unicorn::memory::replace_memory; +use unicorn::unicorn::optimize::{optimize_model_with_input, optimize_model_with_solver}; +use unicorn::unicorn::qubot::{InputEvaluator, Qubot}; +#[cfg(any(feature = "kissat", feature = "cadical", feature = "varisat"))] +use unicorn::unicorn::sat_solver::*; +use unicorn::unicorn::smt_solver::*; + +#[cfg(feature = "boolector")] +use unicorn::unicorn::boolector_impl; +use unicorn::unicorn::unroller::{prune_model, renumber_model, unroll_model}; +use unicorn::unicorn::write_model; +#[cfg(feature = "z3")] +use unicorn::unicorn::z3solver_impl; use ::unicorn::disassemble::disassemble; use ::unicorn::emulate::EmulatorState; @@ -34,6 +39,7 @@ use std::{ str::FromStr, time::Duration, }; +use unicorn::unicorn::quarc::{evaluate_input, QuantumCircuit}; fn main() -> Result<()> { let matches = cli::args().get_matches(); @@ -64,9 +70,9 @@ fn main() -> Result<()> { Ok(()) } - Some(("beator", args)) | Some(("qubot", args)) => { + Some(("beator", args)) | Some(("qubot", args)) | Some(("quarc", args)) => { let is_beator = matches.subcommand().unwrap().0 == "beator"; - + let is_quarc = matches.subcommand().unwrap().0 == "quarc"; let input = expect_arg::(args, "input-file")?; let output = expect_optional_arg::(args, "output-file")?; let unroll = args.get_one::("unroll-model").cloned(); @@ -201,7 +207,33 @@ fn main() -> Result<()> { let gate_model = bitblast_model(&model.unwrap(), true, 64); if sat_solver != SatType::None { - solve_bad_states(&gate_model, sat_solver, terminate_on_bad, one_query)? + match sat_solver { + SatType::None => unreachable!(), + #[cfg(feature = "kissat")] + SatType::Kissat => { + let _ = process_all_bad_states::( + &gate_model, + terminate_on_bad, + one_query, + ); + } + #[cfg(feature = "varisat")] + SatType::Varisat => { + let _ = process_all_bad_states::( + &gate_model, + terminate_on_bad, + one_query, + ); + } + #[cfg(feature = "cadical")] + SatType::Cadical => { + let _ = process_all_bad_states::( + &gate_model, + terminate_on_bad, + one_query, + ); + } + } } if output_to_stdout { @@ -224,6 +256,42 @@ fn main() -> Result<()> { let file = File::create(output_path)?; write_model(&model.unwrap(), file)?; } + } else if is_quarc { + let m = model.unwrap(); + let mut qc = QuantumCircuit::new(&m, 64); // 64 is a paramater describing wordsize + // TODO: make wordsize parameter customizable from command line + let _ = qc.process_model(1); + if has_concrete_inputs { + let inputs = expect_optional_arg::(args, "inputs")?; + let total_variables = qc.input_qubits.len(); + + if let Some(all_inputs) = inputs { + let instances: Vec<&str> = all_inputs.split('-').collect(); + + for instance in instances { + let mut values: Vec = instance + .split(',') + .map(|x| i64::from_str(x).unwrap()) + .collect(); + while values.len() < total_variables { + values.push(0); + } + println!( + "{}\n", + evaluate_input( + &values, + &qc.output_oracle, + &qc.input_qubits, + &qc.circuit_stack, + &qc.dependencies + ) + .0 + ); + } + } else { + panic!("This part of the code should be unreachable."); + } + } } else { let is_ising = args.get_flag("ising"); @@ -274,6 +342,7 @@ fn main() -> Result<()> { Ok(()) } + Some(("dwave", args)) => { let input = args.get_one::("input-file").unwrap(); let runs = *args.get_one::("num-runs").unwrap(); diff --git a/src/unicorn/boolector_impl.rs b/src/unicorn/boolector_impl.rs new file mode 100644 index 00000000..2776d6e2 --- /dev/null +++ b/src/unicorn/boolector_impl.rs @@ -0,0 +1,241 @@ +use crate::unicorn::smt_solver::{SMTSolution, SMTSolver}; +use crate::unicorn::{HashableNodeRef, Node, NodeRef, NodeType}; +use boolector_solver::{ + option::{BtorOption, ModelGen, OutputFileFormat}, + Array, Btor, SolverResult, BV, +}; +use log::debug; +use std::collections::HashMap; +use std::rc::Rc; +use std::time::Duration; + +type ArrayRef = Array>; +type BitVectorRef = BV>; + +#[derive(Clone)] +enum BoolectorValue { + BitVector(BitVectorRef), + Array(ArrayRef), +} + +pub struct BoolectorSolver { + solver: Rc, + mapping: HashMap, +} + +impl SMTSolver for BoolectorSolver { + fn name() -> &'static str { + "Boolector" + } + + fn new(timeout: Option) -> Self { + let solver = Rc::new(Btor::new()); + // TODO: Properly configure the below options. + solver.set_opt(BtorOption::ModelGen(ModelGen::All)); + solver.set_opt(BtorOption::Incremental(true)); + solver.set_opt(BtorOption::OutputFileFormat(OutputFileFormat::SMTLIBv2)); + solver.set_opt(BtorOption::SolverTimeout(timeout)); + Self { + solver, + mapping: HashMap::new(), + } + } + + fn is_always_true(&mut self, node: &NodeRef) -> bool { + let bv = self.visit(node).into_bv().not(); + self.solve_impl(bv) == SMTSolution::Unsat + } + + fn is_always_false(&mut self, node: &NodeRef) -> bool { + let bv = self.visit(node).into_bv(); + self.solve_impl(bv) == SMTSolution::Unsat + } + + fn is_always_equal(&mut self, left: &NodeRef, right: &NodeRef) -> bool { + let bv_left = self.visit(left).into_bv(); + let bv_right = self.visit(right).into_bv(); + let bv = bv_left._ne(&bv_right); + self.solve_impl(bv) == SMTSolution::Unsat + } + + fn solve(&mut self, root: &NodeRef) -> SMTSolution { + let bv = self.visit(root).into_bv(); + self.solve_impl(bv.slice(0, 0)) + } +} + +impl BoolectorSolver { + fn solve_impl(&mut self, bv: BitVectorRef) -> SMTSolution { + self.solver.push(1); + bv.assert(); + let solution = match self.solver.sat() { + SolverResult::Sat => SMTSolution::Sat, + SolverResult::Unsat => SMTSolution::Unsat, + SolverResult::Unknown => SMTSolution::Timeout, + }; + self.solver.pop(1); + if solution == SMTSolution::Timeout { + debug!("Query timeout was reached by Boolector"); + } + solution + } + + fn visit(&mut self, node: &NodeRef) -> BoolectorValue { + let key = HashableNodeRef::from(node.clone()); + self.mapping.get(&key).cloned().unwrap_or_else(|| { + let value = self.translate(node); + assert!(!self.mapping.contains_key(&key)); + self.mapping.insert(key, value.clone()); + value + }) + } + + #[rustfmt::skip] + fn translate(&mut self, node: &NodeRef) -> BoolectorValue { + match &*node.borrow() { + Node::Const { sort, imm, .. } => { + let width = sort.bitsize() as u32; + BV::from_u64(self.solver.clone(), *imm, width).into() + } + Node::Read { memory, address, .. } => { + let array_memory = self.visit(memory).into_array(); + let bv_address = self.visit(address).into_bv(); + array_memory.read(&bv_address).into() + } + Node::Write { memory, address, value, .. } => { + let array_memory = self.visit(memory).into_array(); + let bv_address = self.visit(address).into_bv(); + let bv_value = self.visit(value).into_bv(); + array_memory.write(&bv_address, &bv_value).into() + } + Node::Add { left, right, .. } => { + let bv_left = self.visit(left).into_bv(); + let bv_right = self.visit(right).into_bv(); + bv_left.add(&bv_right).into() + } + Node::Sub { left, right, .. } => { + let bv_left = self.visit(left).into_bv(); + let bv_right = self.visit(right).into_bv(); + bv_left.sub(&bv_right).into() + } + Node::Mul { left, right, .. } => { + let bv_left = self.visit(left).into_bv(); + let bv_right = self.visit(right).into_bv(); + bv_left.mul(&bv_right).into() + } + Node::Divu { left, right, .. } => { + let bv_left = self.visit(left).into_bv(); + let bv_right = self.visit(right).into_bv(); + bv_left.udiv(&bv_right).into() + }, + Node::Div { left, right, .. } => { + let bv_left = self.visit(left).into_bv(); + let bv_right = self.visit(right).into_bv(); + bv_left.sdiv(&bv_right).into() + }, + Node::Rem { left, right, .. } => { + let bv_left = self.visit(left).into_bv(); + let bv_right = self.visit(right).into_bv(); + bv_left.urem(&bv_right).into() + } + Node::Sll { left, right, .. } => { + let bv_left = self.visit(left).into_bv(); + let bv_right = self.visit(right).into_bv(); + bv_left.sll(&bv_right).into() + }, + Node::Srl { left, right, .. } => { + let bv_left = self.visit(left).into_bv(); + let bv_right = self.visit(right).into_bv(); + bv_left.srl(&bv_right).into() + }, + Node::Ult { left, right, .. } => { + let bv_left = self.visit(left).into_bv(); + let bv_right = self.visit(right).into_bv(); + bv_left.ult(&bv_right).into() + } + Node::Ext { from, value, .. } => { + let width = from.bitsize() as u32; + let bv_value = self.visit(value).into_bv(); + assert_eq!(bv_value.get_width(), width); + bv_value.uext(64 - width).into() + } + Node::Ite { sort: NodeType::Memory, cond, left, right, .. } => { + let bv_cond = self.visit(cond).into_bv(); + let array_left = self.visit(left).into_array(); + let array_right = self.visit(right).into_array(); + bv_cond.cond_array(&array_left, &array_right).into() + } + Node::Ite { sort, cond, left, right, .. } => { + let width = sort.bitsize() as u32; + let bv_cond = self.visit(cond).into_bv(); + let bv_left = self.visit(left).into_bv(); + let bv_right = self.visit(right).into_bv(); + assert_eq!(bv_left.get_width(), width); + assert_eq!(bv_right.get_width(), width); + bv_cond.cond_bv(&bv_left, &bv_right).into() + } + Node::Eq { left, right, .. } => { + let bv_left = self.visit(left).into_bv(); + let bv_right = self.visit(right).into_bv(); + bv_left._eq(&bv_right).into() + } + Node::And { left, right, .. } => { + let bv_left = self.visit(left).into_bv(); + let bv_right = self.visit(right).into_bv(); + bv_left.and(&bv_right).into() + } + Node::Or { left, right, .. } => { + let bv_left = self.visit(left).into_bv(); + let bv_right = self.visit(right).into_bv(); + bv_left.or(&bv_right).into() + } + Node::Not { value, .. } => { + let bv_value = self.visit(value).into_bv(); + bv_value.not().into() + } + Node::State { sort: NodeType::Memory, name, .. } => { + Array::new(self.solver.clone(), 64, 64, name.as_deref()).into() + } + Node::State { sort, name, .. } => { + let width = sort.bitsize() as u32; + BV::new(self.solver.clone(), width, name.as_deref()).into() + } + Node::Input { sort, name, .. } => { + let width = sort.bitsize() as u32; + BV::new(self.solver.clone(), width, Some(name)).into() + } + Node::Next { .. } => panic!("should be unreachable"), + Node::Bad { cond, .. } => { + self.visit(cond) + }, + Node::Comment(_) => panic!("cannot translate"), + } + } +} + +impl From for BoolectorValue { + fn from(item: BitVectorRef) -> Self { + Self::BitVector(item) + } +} + +impl From for BoolectorValue { + fn from(item: ArrayRef) -> Self { + Self::Array(item) + } +} + +impl BoolectorValue { + fn into_bv(self) -> BitVectorRef { + match self { + BoolectorValue::BitVector(x) => x, + _ => panic!("expected bit-vector"), + } + } + fn into_array(self) -> ArrayRef { + match self { + BoolectorValue::Array(x) => x, + _ => panic!("expected array"), + } + } +} diff --git a/src/unicorn/btor2file_parser.rs b/src/unicorn/btor2file_parser.rs index 322dd9fc..bbcd02e2 100644 --- a/src/unicorn/btor2file_parser.rs +++ b/src/unicorn/btor2file_parser.rs @@ -45,7 +45,7 @@ fn has_depth_in_name(bad_state: &NodeRef) -> bool { { name.contains("[n=") } else { - panic!("expecting 'Bad' node here"); + false } } diff --git a/src/unicorn/builder.rs b/src/unicorn/builder.rs index 90cc6abe..aa56ffc0 100644 --- a/src/unicorn/builder.rs +++ b/src/unicorn/builder.rs @@ -1,6 +1,11 @@ -use crate::unicorn::{Model, Nid, Node, NodeRef, NodeType}; +use crate::{ + engine, + unicorn::{Model, Nid, Node, NodeRef, NodeType}, + util, +}; use anyhow::{Context, Result}; use byteorder::{ByteOrder, LittleEndian}; +use engine::system::{prepare_unix_stack, SyscallId, NUMBER_OF_REGISTERS}; use log::{debug, trace, warn}; use riscu::{decode, types::*, Instruction, Program, Register}; use std::cell::RefCell; @@ -8,8 +13,7 @@ use std::collections::HashMap; use std::mem::size_of; use std::ops::Range; use std::rc::Rc; -use unicorn::engine::system::{prepare_unix_stack, SyscallId, NUMBER_OF_REGISTERS}; -use unicorn::util::next_multiple_of; +use util::next_multiple_of; // // Public Interface @@ -33,7 +37,7 @@ pub fn generate_model( // const INSTRUCTION_SIZE: u64 = riscu::INSTRUCTION_SIZE as u64; -const PAGE_SIZE: u64 = unicorn::engine::system::PAGE_SIZE as u64; +const PAGE_SIZE: u64 = engine::system::PAGE_SIZE as u64; const WORD_SIZE_MASK: u64 = riscu::WORD_SIZE as u64 - 1; const BITS_PER_BYTE: u64 = 8; diff --git a/src/unicorn/cnf.rs b/src/unicorn/cnf.rs index 8d1ab9a4..2802e2af 100644 --- a/src/unicorn/cnf.rs +++ b/src/unicorn/cnf.rs @@ -50,6 +50,12 @@ impl CNFBuilder { } } +impl Default for CNFBuilder { + fn default() -> Self { + Self::new() + } +} + // // Private Implementation // diff --git a/src/unicorn/codegen.rs b/src/unicorn/codegen.rs index 448621b6..07729dbf 100644 --- a/src/unicorn/codegen.rs +++ b/src/unicorn/codegen.rs @@ -1,11 +1,12 @@ use crate::unicorn::emulate_loader::{name_to_pc_value, name_to_register}; use crate::unicorn::{Model, Node, NodeRef, NodeType}; +use crate::{disassemble, emulate, engine}; use byteorder::{ByteOrder, LittleEndian}; +use disassemble::Disassembly; +use emulate::{EmulatorState, EmulatorValue}; +use engine::system::NUMBER_OF_REGISTERS; use log::{debug, info, trace, warn}; use riscu::{decode, DecodedProgram, Instruction, Program, ProgramSegment, Register}; -use unicorn::disassemble::Disassembly; -use unicorn::emulate::{EmulatorState, EmulatorValue}; -use unicorn::engine::system::NUMBER_OF_REGISTERS; // // Public Interface diff --git a/src/unicorn/emulate_loader.rs b/src/unicorn/emulate_loader.rs index bba7a710..ac19b382 100644 --- a/src/unicorn/emulate_loader.rs +++ b/src/unicorn/emulate_loader.rs @@ -1,8 +1,11 @@ -use crate::unicorn::{Model, Node, NodeRef, NodeType}; +use crate::{ + emulate, engine, + unicorn::{Model, Node, NodeRef, NodeType}, +}; +use emulate::{EmulatorState, EmulatorValue}; +use engine::system::NUMBER_OF_REGISTERS; use log::{debug, trace, warn}; use riscu::Register; -use unicorn::emulate::{EmulatorState, EmulatorValue}; -use unicorn::engine::system::NUMBER_OF_REGISTERS; // // Public Interface diff --git a/src/unicorn/mod.rs b/src/unicorn/mod.rs index a10ac26c..9d54807c 100644 --- a/src/unicorn/mod.rs +++ b/src/unicorn/mod.rs @@ -12,6 +12,8 @@ use std::rc::Rc; pub mod bitblasting; pub mod bitblasting_dimacs; pub mod bitblasting_printer; +#[cfg(feature = "boolector")] +pub mod boolector_impl; pub mod btor2file_parser; pub mod builder; pub mod cnf; @@ -20,10 +22,13 @@ pub mod dimacs_parser; pub mod emulate_loader; pub mod memory; pub mod optimize; +pub mod quarc; pub mod qubot; pub mod sat_solver; pub mod smt_solver; pub mod unroller; +#[cfg(feature = "z3")] +pub mod z3solver_impl; pub type Nid = u64; pub type NodeRef = Rc>; diff --git a/src/unicorn/quarc.rs b/src/unicorn/quarc.rs new file mode 100644 index 00000000..99544e59 --- /dev/null +++ b/src/unicorn/quarc.rs @@ -0,0 +1,3237 @@ +use crate::unicorn::{get_nid, HashableNodeRef, Model, Nid, Node, NodeRef, NodeType}; +use anyhow::Result; +use std::cell::RefCell; +use std::cmp::max; +use std::collections::{HashMap, HashSet, VecDeque}; +use std::fs::File; +use std::hash::{Hash, Hasher}; +use std::io::Write; +use std::rc::Rc; + +// +// Public Interface +// + +// TODO: MAYBE CX gates are not needed. (We can just push the control qubit to the result) +// BEGIN structs declaration +pub type UnitaryRef = Rc>; + +#[derive(Debug)] +pub enum Unitary { + Not { + input: QubitRef, + }, + Cnot { + control: QubitRef, + target: QubitRef, + }, + Mcx { + controls: Vec, + target: QubitRef, + }, + Barrier, +} + +impl From for UnitaryRef { + fn from(unitary: Unitary) -> Self { + Rc::new(RefCell::new(unitary)) + } +} + +#[derive(Debug)] +pub struct HashableUnitaryRef { + pub value: UnitaryRef, +} + +impl Eq for HashableUnitaryRef {} + +impl From for HashableUnitaryRef { + fn from(node: UnitaryRef) -> Self { + Self { value: node } + } +} + +impl Hash for HashableUnitaryRef { + fn hash(&self, state: &mut H) { + RefCell::as_ptr(&self.value).hash(state); + } +} + +impl PartialEq for HashableUnitaryRef { + fn eq(&self, other: &Self) -> bool { + RefCell::as_ptr(&self.value) == RefCell::as_ptr(&other.value) + } +} + +#[derive(Debug)] +pub enum Qubit { + ConstTrue, + ConstFalse, + QBit { + name: String, + dependency: Option, + stack: VecDeque, + }, +} + +impl From for QubitRef { + fn from(gate: Qubit) -> Self { + Rc::new(RefCell::new(gate)) + } +} + +pub type QubitRef = Rc>; + +#[derive(Debug)] +pub struct HashableQubitRef { + pub value: QubitRef, +} + +impl Eq for HashableQubitRef {} + +impl From for HashableQubitRef { + fn from(node: QubitRef) -> Self { + Self { value: node } + } +} + +impl Hash for HashableQubitRef { + fn hash(&self, state: &mut H) { + RefCell::as_ptr(&self.value).hash(state); + } +} + +impl PartialEq for HashableQubitRef { + fn eq(&self, other: &Self) -> bool { + RefCell::as_ptr(&self.value) == RefCell::as_ptr(&other.value) + } +} + +#[derive(Debug)] +pub struct Dependency { + id: u64, + name: String, + operands: Vec>, +} + +impl From for DependencyRef { + fn from(unitary: Dependency) -> Self { + Rc::new(RefCell::new(unitary)) + } +} + +impl Dependency { + pub fn new(id: u64, name: &str, operand1: &[QubitRef], operand2: &[QubitRef]) -> Self { + Self { + id, + name: name.to_string(), + operands: vec![operand1.to_owned(), operand2.to_owned()], + } + } +} + +pub type DependencyRef = Rc>; +#[derive(Debug)] +pub struct HashableDependencyRef { + pub value: DependencyRef, +} + +impl Eq for HashableDependencyRef {} + +impl From for HashableDependencyRef { + fn from(node: DependencyRef) -> Self { + Self { value: node } + } +} + +impl Hash for HashableDependencyRef { + fn hash(&self, state: &mut H) { + RefCell::as_ptr(&self.value).hash(state); + } +} + +impl PartialEq for HashableDependencyRef { + fn eq(&self, other: &Self) -> bool { + RefCell::as_ptr(&self.value) == RefCell::as_ptr(&other.value) + } +} +// END structs declaration + +// BEGIN some functions + +fn get_qubit_from_constant_bit(bit: u64) -> QubitRef { + assert!((bit == 0) | (bit == 1)); + if bit == 1 { + QubitRef::from(Qubit::ConstTrue) + } else { + QubitRef::from(Qubit::ConstFalse) + } +} + +fn get_qubitset_from_constant(value: &u64, wordsize: &usize) -> Vec { + let mut temp = *value; + let mut answer = Vec::new(); + for _ in 0..(*wordsize) { + answer.push(get_qubit_from_constant_bit(temp % 2)); + temp /= 2; + } + answer +} + +fn get_qubit_from_bool(bit: bool) -> QubitRef { + if bit { + QubitRef::from(Qubit::ConstTrue) + } else { + QubitRef::from(Qubit::ConstFalse) + } +} + +fn is_constant(qubit_type: &QubitRef) -> bool { + matches!(&*qubit_type.borrow(), Qubit::ConstFalse | Qubit::ConstTrue) +} + +fn get_value_in_bin(value_: i64, sort: usize) -> Vec { + let mut value = value_; + let mut answer: Vec = Vec::new(); + for _ in 0..sort { + if value % 2 == 0 { + answer.push(false); + } else { + answer.push(true); + } + value /= 2; + } + assert!(sort == answer.len()); + answer +} + +fn get_replacement_from_constant(sort: &NodeType, mut value: u64) -> Vec { + let total_bits = sort.bitsize(); + let mut replacement: Vec = Vec::new(); + for _ in 0..total_bits { + replacement.push(get_qubit_from_constant_bit(value % 2)); + value /= 2; + } + replacement +} + +fn get_value_from_constants(qubits: &[QubitRef]) -> u64 { + let mut answer = 0; + for (index, qubit) in qubits.iter().enumerate() { + assert!(is_constant(qubit)); + + if let Some(value) = get_constant(qubit) { + if value { + answer += 1 << index; + } + } + } + answer +} + +fn are_all_constants(qubits: &[QubitRef]) -> bool { + for qubit in qubits { + if get_constant(qubit).is_none() { + return false; + } + } + true +} + +fn get_word_value( + qubits: &[QubitRef], + assignment: &HashMap, +) -> Option { + let mut answer: i64 = 0; + let mut curr_power = 1; + for qubit in qubits.iter() { + let key = HashableQubitRef::from(qubit.clone()); + if let Some(value) = assignment.get(&key) { + answer += curr_power * (*value as i64); + } else if matches!(&*qubit.borrow(), Qubit::ConstTrue) { + answer += curr_power; + } else if !matches!(&*qubit.borrow(), Qubit::ConstFalse) { + return None; + } + curr_power <<= 1; + } + Some(answer) +} + +pub fn get_constant(gate_type: &QubitRef) -> Option { + match &*gate_type.borrow() { + Qubit::ConstFalse => Some(false), + Qubit::ConstTrue => Some(true), + _ => None, + } +} + +fn are_both_constants(const1: Option, const2: Option) -> bool { + if let Some(_a) = const1 { + if let Some(_b) = const2 { + return true; + } + } + false +} + +fn are_there_false_constants(consts: Vec>) -> bool { + for c in consts.into_iter().flatten() { + if !c { + return true; + } + } + false +} + +fn are_there_true_constants(consts: Vec>) -> bool { + for c in consts.into_iter().flatten() { + if c { + return true; + } + } + false +} + +fn is_target_in_controls(controls: &[QubitRef], target: &QubitRef) -> bool { + let key_target = HashableQubitRef::from(target.clone()); + + for c in controls.iter() { + assert!(!is_constant(c)); + let c_key = HashableQubitRef::from(c.clone()); + + if c_key == key_target { + return true; + } + } + + false +} + +fn prepare_controls_for_mcx( + controls: &[QubitRef], + _target: &QubitRef, +) -> (Option, Vec) { + let mut is_used: HashSet = HashSet::new(); + // is_used.insert(target_key); // TODO: manage properly when target is also control + + let mut result: Vec = Vec::new(); + for q in controls { + if !is_constant(q) { + let key = HashableQubitRef::from(q.clone()); + if !is_used.contains(&key) { + is_used.insert(key); + result.push(q.clone()); + } + } else { + let val = get_constant(q); + if are_there_false_constants(vec![val]) { + return (Some(false), vec![]); + } + } + } + + if result.is_empty() { + // if !is_target_also_control { + // (Some(true), result) + // } else + // if let Some(target_value) = get_constant(target) { + // if target_value { + // (Some(true), result) + // } else { + // (Some(false), result) + // } + // } else { + // target is also control + // (None, result) + (Some(true), result) + // } + } else { + (None, result) + } +} + +// END some functions + +// Begin implementation + +pub fn solve_dependency( + dependency: DependencyRef, + assignments: &mut HashMap, + dependencies_values: &mut HashSet, + dependencies: &HashMap>, +) { + let dep_key = HashableDependencyRef::from(dependency.clone()); + if !dependencies_values.contains(&dep_key) { + let dep = dependency.as_ref().borrow(); + let operands = &dep.operands; + let name = &dep.name; + let operand1_value = get_word_value(&operands[0].clone(), assignments).unwrap(); + let operand2_value = get_word_value(&operands[1], assignments).unwrap(); + assert!(operands[0].len() == operands[1].len()); + let mut result; + if operand2_value != 0 { + if name == "div" { + result = operand1_value / operand2_value; + } else { + assert!(name == "rem"); + + result = operand1_value % operand2_value; + } + } else { + result = operand1_value; + } + + let target = dependencies.get(&dep_key).unwrap(); + for qubit in target.iter() { + let key = HashableQubitRef::from(qubit.clone()); + assignments.insert(key, (result % 2) == 1); + result /= 2; + } + dependencies_values.insert(dep_key); + } +} + +pub fn get_qubit_dependecy(qubit: &QubitRef) -> Option<(u64, String, Vec>)> { + if let Qubit::QBit { + dependency: Some(dep), + .. + } = &*qubit.borrow() + { + let dep = dep.as_ref().borrow(); + let operands = dep.operands.clone(); + let name = dep.name.clone(); + Some((dep.id, name, operands)) + } else { + None + } +} + +pub fn get_dependency_data(hdep: &HashableDependencyRef) -> (u64, String, Vec>) { + let dep = hdep.value.as_ref().borrow(); + let operands = dep.operands.clone(); + let name = dep.name.clone(); + (dep.id, name, operands) +} + +pub fn try_solve_dependency( + assignments: &mut HashMap, + qubit: &QubitRef, + dependecies_values: &mut HashSet, + dependencies: &HashMap>, +) { + if let Qubit::QBit { + dependency: Some(dep), + .. + } = &*qubit.borrow() + { + solve_dependency(dep.clone(), assignments, dependecies_values, dependencies); + } +} + +pub fn evaluate_circuit( + assignments: &mut HashMap, + circuit_stack: &[UnitaryRef], + dependencies: &HashMap>, +) { + let mut dependencies_values: HashSet = HashSet::new(); + for gate in circuit_stack.iter() { + match &*gate.borrow() { + Unitary::Not { input } => { + try_solve_dependency(assignments, input, &mut dependencies_values, dependencies); + let key = HashableQubitRef::from(input.clone()); + + if assignments.contains_key(&key) { + let value = *assignments.get(&key).unwrap(); + assignments.insert(key, !value); + } else { + // qubits are initialized in 0. Therefore, NOT should set it to true. + assignments.insert(key, true); + } + } + Unitary::Cnot { control, target } => { + assert!(!is_constant(control)); + assert!(!is_constant(target)); + try_solve_dependency(assignments, control, &mut dependencies_values, dependencies); + try_solve_dependency(assignments, target, &mut dependencies_values, dependencies); + + let control_key = HashableQubitRef::from(control.clone()); + let target_key = HashableQubitRef::from(target.clone()); + + if let Some(control_value) = assignments.get(&control_key) { + if *control_value { + if let Some(target_value) = assignments.get(&target_key) { + if *target_value { + assignments.insert(target_key, false); + } else { + assignments.insert(target_key, true); + } + } else { + // target is initialized in 0, therefore we must flip it to 1 + assignments.insert(target_key, true); + } + } else if assignments.get(&target_key).is_none() { + // if control is not true we just check if its in the assignments-dictionary, if not we add it + assignments.insert(target_key, false); + } + } else { + panic!("Control qubit does not has any value! There is a bug."); + } + } + Unitary::Mcx { controls, target } => { + assert!(!controls.is_empty()); + try_solve_dependency(assignments, target, &mut dependencies_values, dependencies); + let mut controls_and = true; + for control in controls { + try_solve_dependency( + assignments, + control, + &mut dependencies_values, + dependencies, + ); + let control_key = HashableQubitRef::from(control.clone()); + if let Some(control_val) = assignments.get(&control_key) { + if !(*control_val) { + controls_and = false; + break; + } + } else { + panic!( + "There is a control in MCX that doesnt has a value. This is a bug {:?}", + control + ); + } + } + let target_key = HashableQubitRef::from(target.clone()); + + if controls_and { + if let Some(target_value) = assignments.get(&target_key) { + if *target_value { + assignments.insert(target_key, false); + } else { + assignments.insert(target_key, true); + } + } else { + assignments.insert(target_key, true); + } + } else if assignments.get(&target_key).is_none() { + // if control is not true we just check if its in the assignments-dictionary, if not we add it + assignments.insert(target_key, false); + } + } + Unitary::Barrier => {} + } + } +} + +pub fn evaluate_input( + values: &[i64], + output_oracle: &Option, + input_qubits: &[(NodeRef, Vec)], + circuit_stack: &[UnitaryRef], + dependencies: &HashMap>, +) -> (bool, HashMap) { + assert!(output_oracle.is_some()); + let mut assignments: HashMap = HashMap::new(); + // if let Some(value) = get_constant(&self.output_oracle.clone().unwrap()) { + // return (value, assignments); + // } + + for (input, value) in input_qubits.iter().zip(values.iter()) { + let qubits = input.1.clone(); + let bin_value = get_value_in_bin(*value, qubits.len()); + + for (qubit, bit) in qubits.iter().zip(bin_value.iter()) { + let key = HashableQubitRef::from(qubit.clone()); + assignments.insert(key, *bit); + } + } + + evaluate_circuit(&mut assignments, circuit_stack, dependencies); + if let Some(value) = get_constant(&output_oracle.clone().unwrap()) { + (value, assignments) + } else { + let key = HashableQubitRef::from(output_oracle.as_ref().unwrap().clone()); + return (*assignments.get(&key).unwrap(), assignments); + } +} + +pub struct QuantumCircuit<'a> { + pub bad_state_qubits: Vec, + pub bad_state_nodes: Vec, + pub all_qubits: HashSet, + pub constraints: HashMap, // this is for remainder and division, these are constraint based. + pub qubit_to_nid: HashMap, + pub dependencies: HashMap>, + pub input_qubits: Vec<(NodeRef, Vec)>, + pub mapping_nids: HashMap, + pub mapping: HashMap>>, // maps a btor2 operator to its resulting bitvector of gates + pub circuit_stack: Vec, + pub count_multiqubit_gates: u64, + pub current_n: i32, + pub current_state_nodes: HashMap, + pub result_ored_bad_states: QubitRef, + pub dynamic_memory: Vec, + pub output_oracle: Option, + clean_ancillas: HashSet, + used_ancillas: HashSet, + // pub temp: Vec, + word_size: usize, + model: &'a Model, // BTOR2 model +} + +impl<'a> QuantumCircuit<'a> { + pub fn new(model_: &'a Model, word_size_: usize) -> Self { + Self { + bad_state_qubits: Vec::new(), + bad_state_nodes: Vec::new(), + constraints: HashMap::new(), + dependencies: HashMap::new(), + all_qubits: HashSet::new(), + input_qubits: Vec::new(), + mapping_nids: HashMap::new(), + mapping: HashMap::new(), + dynamic_memory: Vec::new(), + circuit_stack: Vec::new(), + current_state_nodes: HashMap::new(), + model: model_, + word_size: word_size_, + count_multiqubit_gates: 0, + current_n: 0, + qubit_to_nid: HashMap::new(), + clean_ancillas: HashSet::new(), + used_ancillas: HashSet::new(), + result_ored_bad_states: QubitRef::from(Qubit::QBit { + name: "result_or".to_string(), + dependency: None, + stack: VecDeque::new(), + }), + output_oracle: None, + } + } + + fn add_not_gate( + &mut self, + qubit: &mut QubitRef, + gates_to_uncompute_: Option<&mut Vec>, + ) -> QubitRef { + if let Some(value) = get_constant(qubit) { + if value { + QubitRef::from(Qubit::ConstFalse) + } else { + QubitRef::from(Qubit::ConstTrue) + } + } else { + let not_gate = UnitaryRef::from(Unitary::Not { + input: qubit.clone(), + }); + self.circuit_stack.push(not_gate.clone()); + + self.add_gate_to_qubit_stack(qubit, not_gate.clone()); + if let Some(gates_to_uncompute) = gates_to_uncompute_ { + gates_to_uncompute.push(not_gate); + } + qubit.clone() + } + } + + fn add_mcx_gate( + &mut self, + controls: Vec<&mut QubitRef>, + target: &mut QubitRef, + gates_to_uncompute_: Option<&mut Vec>, + ) { + let non_mutable_vec = controls + .into_iter() + .map(|x| (*x).clone()) + .collect::>(); + let mcx_gate = UnitaryRef::from(Unitary::Mcx { + controls: non_mutable_vec, + target: target.clone(), + }); + + self.circuit_stack.push(mcx_gate.clone()); + + self.add_gate_to_qubit_stack(target, mcx_gate.clone()); + if let Some(gates_to_uncompute) = gates_to_uncompute_ { + gates_to_uncompute.push(mcx_gate); + } + } + + fn not_gate(&mut self, a_qubit: &mut QubitRef) -> QubitRef { + if let Some(a_const) = get_constant(a_qubit) { + if a_const { + QubitRef::from(Qubit::ConstFalse) + } else { + QubitRef::from(Qubit::ConstTrue) + } + } else { + // since we dont know whether this qubit is going to be used later + let mut target = self.get_rom(None); + + assert!(!is_constant(&target)); + + target = self.add_not_gate(&mut target, None); + self.add_mcx_gate(vec![a_qubit], &mut target, None); + target + } + } + + fn is_qubit_rom(&self, qubit: &QubitRef) -> bool { + let key = HashableQubitRef::from(qubit.clone()); + !self.clean_ancillas.contains(&key) && !self.used_ancillas.contains(&key) + } + + fn is_rom(&self, replacement: &[QubitRef]) -> bool { + for r in replacement.iter() { + if !self.is_qubit_rom(r) { + return false; + } + } + true + } + + fn get_last_qubitset(&self, node: &NodeRef) -> Option> { + let key = HashableNodeRef::from(node.clone()); + + if !self.mapping.contains_key(&key) { + None + } else { + match *node.borrow() { + Node::Const { .. } => { + if self.mapping.get(&key).unwrap().contains_key(&0) { + Some(self.mapping.get(&key).cloned().unwrap()[&0].clone()) + } else { + None + } + } + Node::State { .. } | Node::Input { .. } => { + let replacements = self.mapping.get(&key).unwrap(); + if let Some(replacement) = replacements.get(&(self.current_n - 1)) { + assert!(self.is_rom(replacement)); + Some(replacement.clone()) + } else { + let node_hash = HashableNodeRef::from(node.clone()); + let index = self.current_state_nodes[&node_hash]; + assert!(self.is_rom(&replacements[&index].clone())); + Some(replacements[&index].clone()) + } + } + Node::Next { .. } | Node::Bad { .. } => None, + _ => { + let replacements = self.mapping.get(&key).unwrap(); + if replacements.contains_key(&self.current_n) { + assert!(self.is_rom(&replacements[&self.current_n].clone())); + Some(replacements[&self.current_n].clone()) + } else { + None + } + } + } + } + } + + fn or_bad_state_qubits(&mut self, controls: Vec, target: &QubitRef) { + // This function assumes optimizations before calling it, since its only used for the output of the oracle. + // assume all values are Qubit::Qbit + assert!(controls.len() > 1); + assert!(!is_constant(target)); + self.circuit_stack.push(UnitaryRef::from(Unitary::Not { + input: target.clone(), + })); + + for qubit in controls.iter() { + assert!(!is_constant(qubit)); + self.circuit_stack.push(UnitaryRef::from(Unitary::Not { + input: qubit.clone(), + })); + } + + self.circuit_stack.push(UnitaryRef::from(Unitary::Mcx { + controls, + target: target.clone(), + })); + // for qubit in self.bad_state_qubits.clone() { + // assert!(!is_constant(&qubit)); + // self.circuit_stack + // .push(UnitaryRef::from(Unitary::Not { input: qubit })); + // } + } + + fn _are_all_ancillas_clean(&self) -> bool { + self.used_ancillas.is_empty() + } + + fn apply_mcx_gate_for_target_in_controls( + &mut self, + controls_: &mut [QubitRef], + target: &QubitRef, + gates_to_uncompute: &mut Vec, + is_rom: bool, + ) -> QubitRef { + assert!(!is_constant(target)); + if controls_.len() == 1 { + QubitRef::from(Qubit::ConstFalse) + } else { + let mut controls = Vec::new(); + + let target_key = HashableQubitRef::from(target.clone()); + for c in controls_.iter() { + let c_key = HashableQubitRef::from(c.clone()); + if c_key != target_key { + controls.push(c.clone()); + } + } + let mut local_gates_to_uncompute: Vec = Vec::new(); + + let mut ancilla_controls = self.get_memory(); + self.add_mcx_gate( + controls.iter_mut().collect(), + &mut target.clone(), + Some(&mut local_gates_to_uncompute), + ); + ancilla_controls = + self.add_not_gate(&mut ancilla_controls, Some(&mut local_gates_to_uncompute)); + + let mut qubit_out = if is_rom { + self.get_rom(None) + } else { + self.get_memory() + }; + + if !is_rom { + for gate in local_gates_to_uncompute { + gates_to_uncompute.push(gate); + } + self.add_mcx_gate( + vec![&mut ancilla_controls, &mut target.clone()], + &mut qubit_out, + Some(gates_to_uncompute), + ); + } else { + self.add_mcx_gate( + vec![&mut ancilla_controls, &mut target.clone()], + &mut qubit_out, + None, + ); + let prev_length = self.used_ancillas.len(); + self.uncompute(&local_gates_to_uncompute); + assert!(self.used_ancillas.len() == prev_length - 1); + } + qubit_out + } + } + + fn apply_mcx_gate( + &mut self, + controls_: &mut [QubitRef], + target_: &Option, + gates_to_uncompute: &mut Vec, + is_rom: bool, + allow_push: bool, + ) -> QubitRef { + let mut target = if let Some(qubit) = target_ { + if is_rom && !self.is_qubit_rom(qubit) { + let new_target = QubitRef::from(Qubit::QBit { + name: "".to_string(), + dependency: None, + stack: VecDeque::new(), + }); + self.circuit_stack.push(UnitaryRef::from(Unitary::Cnot { + control: qubit.clone(), + target: new_target.clone(), + })); + new_target + } else { + qubit.clone() + } + } else { + QubitRef::from(Qubit::ConstFalse) + }; + + if is_rom { + assert!(self.is_qubit_rom(&target)); + } + + let (value_, mut controls) = prepare_controls_for_mcx(controls_, &target); + + if is_target_in_controls(&controls, &target) { + return self.apply_mcx_gate_for_target_in_controls( + &mut controls, + &target, + gates_to_uncompute, + is_rom, + ); + } + + if let Some(value) = value_ { + if value { + // all controls are true + if let Some(target_val) = get_constant(&target) { + // all controls are true and target is a constant + if target_val { + QubitRef::from(Qubit::ConstFalse) + } else { + QubitRef::from(Qubit::ConstTrue) + } + } else { + if !is_rom { + target = self.add_not_gate(&mut target, Some(gates_to_uncompute)); + } else { + assert!(self.is_qubit_rom(&target)); + target = self.add_not_gate(&mut target, None); + } + target + } + } else { + // at least one control is false + if is_rom { + assert!(self.is_qubit_rom(&target)); + } + target + } + } else { + let target_ghost_value = if let Some(v) = get_constant(&target) { + if allow_push { + v + } else { + true + } + } else { + true + }; + + if controls.len() == 1 && !target_ghost_value { + controls[0].clone() + } else { + let mut target_final; + if let Some(target_value) = get_constant(&target) { + if is_rom { + target_final = self.get_rom(None); + } else { + target_final = self.get_memory(); + } + + if target_value { + if !is_rom { + target_final = + self.add_not_gate(&mut target_final, Some(gates_to_uncompute)); + } else { + target_final = self.add_not_gate(&mut target_final, None); + } + } + if !is_rom { + self.add_mcx_gate( + controls.iter_mut().collect(), + &mut target_final, + Some(gates_to_uncompute), + ); + } else { + self.add_mcx_gate(controls.iter_mut().collect(), &mut target_final, None); + } + } else { + target_final = target; + if !is_rom { + self.add_mcx_gate( + controls.iter_mut().collect(), + &mut target_final, + Some(gates_to_uncompute), + ); + } else { + self.add_mcx_gate(controls.iter_mut().collect(), &mut target_final, None); + } + } + if is_rom { + assert!(self.is_qubit_rom(&target_final)); + } + target_final + } + } + } + + fn record_mapping( + &mut self, + node: &NodeRef, + index: i32, + replacement: Vec, + ) -> Vec { + let key = HashableNodeRef::from(node.clone()); + + if !self.mapping.contains_key(&key) { + self.mapping.insert(key.clone(), HashMap::new()); + } + + let replacements = self.mapping.get_mut(&key).unwrap(); + replacements.insert(index, replacement.clone()); + self.current_state_nodes.insert(key, index); + + replacement + } + + fn process_input(&mut self, sort: usize, node: &NodeRef, _name: String) -> Vec { + if let Some(replacement) = self.get_last_qubitset(node) { + replacement + } else { + let mut replacement: Vec = Vec::new(); + for _ in 0..sort { + replacement.push(self.get_rom(None)); + } + self.input_qubits.push((node.clone(), replacement.clone())); + assert!(replacement.len() == sort); + assert!(self.is_rom(&replacement)); + self.record_mapping(node, self.current_n, replacement) + } + } + fn pop_back_qubit_stack(&mut self, qubit: &QubitRef, gate: &UnitaryRef) { + // assert!(!self.is_qubit_rom(qubit)); + + match *qubit.borrow_mut() { + Qubit::QBit { ref mut stack, .. } => { + assert!(!stack.is_empty()); + let qubit_key = HashableQubitRef::from(qubit.clone()); + let gate_qubit_stack = stack.pop_back().unwrap(); + let gate_key = HashableUnitaryRef::from(gate.clone()); + let gate_qubit = HashableUnitaryRef::from(gate_qubit_stack); + assert!(gate_key == gate_qubit); + + if stack.is_empty() && !self.is_qubit_rom(qubit) { + assert!(self.used_ancillas.contains(&qubit_key)); + self.used_ancillas.remove(&qubit_key); + self.clean_ancillas.insert(qubit_key); + } + } + _ => panic!("Trying to pop stack of constant qubit!"), + } + } + + fn get_dependency(&self, qubit: &QubitRef) -> Option { + match &*qubit.borrow() { + Qubit::QBit { dependency, .. } => dependency.clone(), + _ => None, + } + } + + fn get_qubit_stack_length(&mut self, qubit: &QubitRef) -> usize { + match &*qubit.borrow() { + Qubit::QBit { stack, .. } => stack.len(), + _ => panic!("Trying to get length of constant bit"), + } + } + + fn get_safe_uncomputable_rom( + &mut self, + gates_to_uncompute: &[UnitaryRef], + replacement: &[QubitRef], + ) -> Vec { + let mut new_replacement = Vec::new(); + + let mut non_const_qubits = HashSet::new(); + for gate in gates_to_uncompute.iter() { + if let Some(qubit) = self.get_qubit_to_uncompute(gate) { + let qubit_key = HashableQubitRef::from(qubit.clone()); + non_const_qubits.insert(qubit_key); + } + } + + for r in replacement.iter() { + let r_key = HashableQubitRef::from(r.clone()); + assert!(self.is_qubit_rom(r)); + if non_const_qubits.contains(&r_key) { + let dep = self.get_dependency(r); + let new_qubit = self.get_rom(dep); + self.circuit_stack.push(UnitaryRef::from(Unitary::Cnot { + control: r.clone(), + target: new_qubit.clone(), + })); + new_replacement.push(new_qubit); + } else { + new_replacement.push(r.clone()); + } + } + assert!(new_replacement.len() == replacement.len()); + new_replacement + } + + fn get_qubit_to_uncompute(&self, gate: &UnitaryRef) -> Option { + match &*gate.borrow() { + Unitary::Not { input } => Some(input.clone()), + Unitary::Cnot { control: _, target } => Some(target.clone()), + Unitary::Mcx { + controls: _, + target, + } => Some(target.clone()), + Unitary::Barrier => None, + } + } + + fn uncompute(&mut self, gates_to_uncompute: &[UnitaryRef]) { + for gate in gates_to_uncompute.iter().rev() { + self.circuit_stack.push(gate.clone()); + if let Some(qubit) = self.get_qubit_to_uncompute(gate) { + let previous_length = self.get_qubit_stack_length(&qubit); + self.pop_back_qubit_stack(&qubit, gate); + assert!(previous_length - 1 == self.get_qubit_stack_length(&qubit)); + } + } + } + + fn get_rom(&mut self, dependency_: Option) -> QubitRef { + if let Some(dependency) = dependency_ { + QubitRef::from(Qubit::QBit { + name: "".to_string(), + dependency: Some(dependency), + stack: VecDeque::new(), + }) + } else { + QubitRef::from(Qubit::QBit { + name: "".to_string(), + dependency: None, + stack: VecDeque::new(), + }) + } + } + + fn get_one_clean_ancilla(&mut self) -> QubitRef { + if self.clean_ancillas.is_empty() { + panic!("There are no ancillas"); + } + let element = self.clean_ancillas.iter().next().unwrap(); + element.value.clone() + } + + fn get_memory(&mut self) -> QubitRef { + if self.clean_ancillas.is_empty() { + let key = HashableQubitRef::from(QubitRef::from(Qubit::QBit { + name: "".to_string(), + dependency: None, + stack: VecDeque::new(), + })); + self.clean_ancillas.insert(key); + } + + let qubit = self.get_one_clean_ancilla(); + + match &*qubit.borrow() { + Qubit::QBit { stack, .. } => { + assert!(stack.is_empty()); + } + _ => { + panic!("memory has constant value!"); + } + } + let key = HashableQubitRef::from(qubit.clone()); + self.clean_ancillas.remove(&key); + self.used_ancillas.insert(key); + qubit + } + + fn add_one_qubitset( + &mut self, + qubitset: &[QubitRef], + target_set: Vec, + gates_to_uncompute: &mut Vec, + is_rom: bool, + ) -> Vec { + let mut result: Vec = vec![]; + + let sort = qubitset.len(); + assert!(target_set.len() == qubitset.len()); + + for qubit in target_set.iter() { + result.push(qubit.clone()); + } + + for index in 0..sort { + for i in index..sort { + let mut controls = result[index..((sort - 1 - i) + index)].to_vec(); + controls.push(qubitset[index].clone()); + let target = result[sort - 1 - i + index].clone(); + + result[sort - 1 - i + index] = self.apply_mcx_gate( + &mut controls, + &Some(target), + gates_to_uncompute, + is_rom, + false, + ); + } + } + assert!(result.len() == sort); + result + } + + fn add_gate_to_qubit_stack(&mut self, qubit: &mut QubitRef, gate: UnitaryRef) { + let key = HashableQubitRef::from(qubit.clone()); + self.clean_ancillas.remove(&key); + + assert!(!self.clean_ancillas.contains(&key)); + match *qubit.borrow_mut() { + Qubit::QBit { ref mut stack, .. } => { + let prev_length = stack.len(); + stack.push_back(gate); + assert!(stack.len() == prev_length + 1); + } + _ => panic!("parameter of this function should not be a constant value"), + } + } + + fn add( + &mut self, + left_operand: &[QubitRef], + right_operand: &[QubitRef], + gates_to_uncompute: &mut Vec, + is_rom: bool, + ) -> Vec { + assert!(left_operand.len() == right_operand.len()); + let mut replacement: Vec = vec![]; + + // initially replacement is |0> + for _ in 0..left_operand.len() { + replacement.push(QubitRef::from(Qubit::ConstFalse)); + } + + // replacement += left_operand + replacement = self.add_one_qubitset(left_operand, replacement, gates_to_uncompute, false); + + // replacement += right_operand + replacement = self.add_one_qubitset(right_operand, replacement, gates_to_uncompute, is_rom); + assert!(replacement.len() == left_operand.len()); + replacement + } + + fn sub( + &mut self, + left_operand: &[QubitRef], + right_operand: &[QubitRef], + gates_to_uncompute: &mut Vec, + is_rom: bool, + ) -> Vec { + assert!(left_operand.len() == right_operand.len()); + let (to_uncompute, negated_right) = self.twos_complement(right_operand); + + let replacement = self.add(left_operand, &negated_right, gates_to_uncompute, is_rom); + + // uncompute twos complement + for gate in to_uncompute.iter().rev() { + self.circuit_stack.push(gate.clone()); + } + + assert!(replacement.len() == left_operand.len()); + replacement + } + + fn twos_complement(&mut self, qubitset: &[QubitRef]) -> (Vec, Vec) { + let mut gates_to_uncompute: Vec = Vec::new(); + let mut result1: Vec = Vec::new(); + + for qubit in qubitset { + if let Some(val) = get_constant(qubit) { + if val { + result1.push(QubitRef::from(Qubit::ConstFalse)); + } else { + result1.push(QubitRef::from(Qubit::ConstTrue)); + } + } else { + result1.push(qubit.clone()); + assert!(!is_constant(qubit)); + gates_to_uncompute.push(UnitaryRef::from(Unitary::Not { + input: qubit.clone(), + })); + self.circuit_stack.push(UnitaryRef::from(Unitary::Not { + input: qubit.clone(), + })); + } + } + assert!(result1.len() == qubitset.len()); + let sort = qubitset.len(); + for i in 0..sort - 1 { + let target = result1[sort - i - 1].clone(); + let mut controls = result1[..(sort - i - 1)].to_vec(); + result1[sort - i - 1] = self.apply_mcx_gate( + &mut controls, + &Some(target), + &mut gates_to_uncompute, + false, + false, + ); + } + + assert!(result1.len() == qubitset.len()); + + // apply not gate to LSB qubit + if let Some(val) = get_constant(&result1[0]) { + result1[0] = get_qubit_from_bool(!val); + } else { + assert!(!is_constant(&result1[0])); + gates_to_uncompute.push(UnitaryRef::from(Unitary::Not { + input: result1[0].clone(), + })); + self.circuit_stack.push(UnitaryRef::from(Unitary::Not { + input: result1[0].clone(), + })); + } + + (gates_to_uncompute, result1) + } + + fn multiply_word_by_bit( + &mut self, + word: &[QubitRef], + bit: &QubitRef, + shift: usize, + gates_to_uncompute: &mut Vec, + is_rom: bool, + ) -> Vec { + let mut result: Vec = Vec::new(); + + let mut s = 0; + let mut i = 0; + if let Some(val) = get_constant(bit) { + if val { + while result.len() < word.len() { + if s < shift { + result.push(QubitRef::from(Qubit::ConstFalse)); + s += 1; + } else { + result.push(word[i].clone()); + i += 1; + } + } + } else { + while result.len() < word.len() { + result.push(QubitRef::from(Qubit::ConstFalse)); + } + } + result + } else { + while result.len() < word.len() { + if s < shift { + result.push(QubitRef::from(Qubit::ConstFalse)); + s += 1; + } else { + if let Some(val) = get_constant(&word[i]) { + if val { + result.push(bit.clone()); + } else { + result.push(QubitRef::from(Qubit::ConstFalse)); + } + } else { + let target = self.apply_mcx_gate( + &mut [word[i].clone(), bit.clone()], + &None, + gates_to_uncompute, + is_rom, + false, + ); + result.push(target.clone()); + } + i += 1; + } + } + assert!(result.len() == word.len()); + result + } + } + + fn mul( + &mut self, + left_operand: &[QubitRef], + right_operand: &[QubitRef], + gates_to_uncompute: &mut Vec, + is_rom: bool, + ) -> Vec { + assert!(left_operand.len() == right_operand.len()); + let mut replacement: Vec = Vec::new(); + + for _ in 0..left_operand.len() { + replacement.push(QubitRef::from(Qubit::ConstFalse)); + } + for (index, bit) in left_operand.iter().enumerate() { + let result = + self.multiply_word_by_bit(right_operand, bit, index, gates_to_uncompute, false); + + if index + 1 == left_operand.len() { + replacement = + self.add_one_qubitset(&result, replacement, gates_to_uncompute, is_rom); + } else { + replacement = + self.add_one_qubitset(&result, replacement, gates_to_uncompute, false); + } + } + assert!(replacement.len() == left_operand.len()); + replacement + } + + fn eq( + &mut self, + left_operand: &[QubitRef], + right_operand: &[QubitRef], + gates_to_uncompute: &mut Vec, + is_rom: bool, + allow_push: bool, + ) -> Vec { + assert!(left_operand.len() == right_operand.len()); + let mut controls: Vec = vec![]; + let mut qubits_to_not: HashSet = HashSet::new(); + let mut qubit_to_not_vec: Vec = Vec::new(); + + for (l_qubit, r_qubit) in left_operand.iter().zip(right_operand.iter()) { + let const_l = get_constant(l_qubit); + let const_r = get_constant(r_qubit); + + if are_both_constants(const_l, const_r) { + if const_l.unwrap() != const_r.unwrap() { + return vec![QubitRef::from(Qubit::ConstFalse)]; + } + } else if are_there_true_constants(vec![const_l, const_r]) { + if is_constant(l_qubit) { + controls.push(r_qubit.clone()); + } else { + controls.push(l_qubit.clone()); + } + } else if are_there_false_constants(vec![const_l, const_r]) { + let control: QubitRef = if is_constant(l_qubit) { + r_qubit.clone() + } else { + l_qubit.clone() + }; + + let target: QubitRef = self.apply_mcx_gate( + &mut [control.clone()], + &None, + gates_to_uncompute, + false, + allow_push, + ); + // controls.push(target.clone()); + assert!(!is_constant(&target)); + let target_key = HashableQubitRef::from(target.clone()); + if !qubits_to_not.contains(&target_key) { + qubits_to_not.insert(target_key); + qubit_to_not_vec.push(target); + } + + // self.add_not_gate(&mut target, Some(gates_to_uncompute)); + } else { + // no constants + let mut target: QubitRef = self.apply_mcx_gate( + &mut [l_qubit.clone()], + &None, + gates_to_uncompute, + false, + allow_push, + ); + + assert!(!is_constant(&target)); + + target = self.apply_mcx_gate( + &mut [r_qubit.clone()], + &Some(target.clone()), + gates_to_uncompute, + false, + true, + ); + + // target = self.add_not_gate(&mut target, Some(gates_to_uncompute)); + // controls.push(target.clone()); + let target_key = HashableQubitRef::from(target.clone()); + if !qubits_to_not.contains(&target_key) { + qubits_to_not.insert(target_key); + qubit_to_not_vec.push(target); + } + } + } + + for q in qubit_to_not_vec.iter_mut() { + controls.push(self.add_not_gate(q, Some(gates_to_uncompute))); + } + + let replacement = + vec![self.apply_mcx_gate(&mut controls, &None, gates_to_uncompute, is_rom, allow_push)]; + assert!(replacement.len() == 1); + replacement + } + + fn insert_into_constraints(&mut self, qubit: &QubitRef, value: bool) { + let key = HashableQubitRef::from(qubit.clone()); + if let std::collections::hash_map::Entry::Vacant(e) = self.constraints.entry(key) { + e.insert(value); + } else { + let key = HashableQubitRef::from(qubit.clone()); + assert!(value == *self.constraints.get(&key).unwrap()); + } + } + + fn div( + &mut self, + left: &NodeRef, + right: &NodeRef, + nid: &Nid, + ) -> (Vec, Vec) { + let mut left_operand = self.process(left); + let mut right_operand = self.process(right); + assert!(self.is_rom(&left_operand)); + assert!(self.is_rom(&right_operand)); + + assert!(left_operand.len() == right_operand.len()); + + if are_all_constants(&left_operand) && are_all_constants(&right_operand) { + let value_left = get_value_from_constants(&left_operand); + let value_right = get_value_from_constants(&right_operand); + + if value_right == 0 { + panic!("There is a division by zero in this program!"); + } + + let coeff_dec = value_left / value_right; + let rem_dec = value_left % value_right; + + let wordsize = left_operand.len(); + let coeff_qubitset = get_qubitset_from_constant(&coeff_dec, &wordsize); + let rem_qubitset = get_qubitset_from_constant(&rem_dec, &wordsize); + + (coeff_qubitset, rem_qubitset) + } else { + let mut c: Vec = Vec::new(); + let mut r: Vec = Vec::new(); + + left_operand.push(QubitRef::from(Qubit::ConstFalse)); + right_operand.push(QubitRef::from(Qubit::ConstFalse)); + + let sort = left_operand.len(); + let mut i = 0; + + let coeff_dep = DependencyRef::from(Dependency::new( + self.dependencies.len() as u64, + "div", + &left_operand, + &right_operand, + )); + let rem_dep = DependencyRef::from(Dependency::new( + self.dependencies.len() as u64, + "rem", + &left_operand, + &right_operand, + )); + while c.len() < sort { + c.push(QubitRef::from(Qubit::QBit { + name: format!("{}_coeff{}_{}", nid, i, self.current_n), + dependency: Some(coeff_dep.clone()), + stack: VecDeque::new(), + })); + r.push(QubitRef::from(Qubit::QBit { + name: format!("{}_rem{}_{}", nid, i, self.current_n), + dependency: Some(rem_dep.clone()), + stack: VecDeque::new(), + })); + i += 1; + } + + let mut key = HashableDependencyRef::from(coeff_dep); + self.dependencies.insert(key, c.clone()); + + key = HashableDependencyRef::from(rem_dep); + self.dependencies.insert(key, r.clone()); + + let mut gates_to_uncompute = Vec::new(); + let res_mul = self.mul(&right_operand, &c, &mut gates_to_uncompute, false); + + let res_sum = self.add(&res_mul, &r, &mut gates_to_uncompute, false); + + let res_eq = self.eq( + &res_sum, + &left_operand, + &mut gates_to_uncompute, + false, + false, + ); + assert!(res_eq.len() == 1); + + let mut gates_to_uncompute = Vec::new(); + let res_ult = self.ult(&r, &right_operand, &true, &mut gates_to_uncompute, false); + + let mut true_constraints_target = self.apply_mcx_gate( + &mut [res_eq[0].clone(), res_ult[res_ult.len() - 1].clone()], + &None, + &mut gates_to_uncompute, + true, + false, + ); + + { + // add the following constraints: + // left = right*coeff + rem + // rem < right + if let Some(value) = get_constant(&true_constraints_target) { + if !value { + panic!("constraints are never met") + } + } else { + // check right operand cannot be zero + let mut dummy_zero: Vec = Vec::new(); + + for _ in 0..right_operand.len() { + dummy_zero.push(QubitRef::from(Qubit::ConstFalse)); + } + + let eq_dummy_zero = self.eq( + &dummy_zero, + &right_operand, + &mut gates_to_uncompute, + false, + false, + ); + assert!(eq_dummy_zero.len() == 1); + + if let Some(div_zero_dummy) = get_constant(&eq_dummy_zero[0]) { + if div_zero_dummy { + panic!("There is a division by zero!"); + } + assert!(self.is_qubit_rom(&true_constraints_target)); + true_constraints_target = self.get_safe_uncomputable_rom( + &gates_to_uncompute, + &[true_constraints_target.clone()], + )[0] + .clone(); + self.insert_into_constraints(&true_constraints_target, true); + } else { + let mut all_constraints_target = self.get_rom(None); + + // or eq_dummy_zero and true constraints + let key_zero_dummy = HashableQubitRef::from(eq_dummy_zero[0].clone()); + let key_true_constraints = + HashableQubitRef::from(true_constraints_target.clone()); + + // NOT operands + self.circuit_stack.push(UnitaryRef::from(Unitary::Not { + input: true_constraints_target.clone(), + })); + if key_zero_dummy != key_true_constraints { + self.circuit_stack.push(UnitaryRef::from(Unitary::Not { + input: eq_dummy_zero[0].clone(), + })); + } + + // NOT target + let key_all_constraints = + HashableQubitRef::from(all_constraints_target.clone()); + assert!(key_all_constraints != key_zero_dummy); + assert!(key_all_constraints != key_true_constraints); + self.circuit_stack.push(UnitaryRef::from(Unitary::Not { + input: all_constraints_target.clone(), + })); + + // PERFORM MCX (logic or) + let (value, controls) = prepare_controls_for_mcx( + &[true_constraints_target.clone(), eq_dummy_zero[0].clone()], + &all_constraints_target, + ); + assert!(value.is_none()); + + self.circuit_stack.push(UnitaryRef::from(Unitary::Mcx { + controls, + target: all_constraints_target.clone(), + })); + assert!(self.is_qubit_rom(&all_constraints_target)); + all_constraints_target = self.get_safe_uncomputable_rom( + &gates_to_uncompute, + &[all_constraints_target.clone()], + )[0] + .clone(); + self.insert_into_constraints(&all_constraints_target, true); + + // Uncompute NOT on operands + self.circuit_stack.push(UnitaryRef::from(Unitary::Not { + input: true_constraints_target.clone(), + })); + if key_zero_dummy != key_true_constraints { + self.circuit_stack.push(UnitaryRef::from(Unitary::Not { + input: eq_dummy_zero[0].clone(), + })); + } + } + } + } + + { + // add overflow constraints + let overflow_qubit_sum = res_sum[res_sum.len() - 1].clone(); + let overflow_qubit_mul = res_mul[res_mul.len() - 1].clone(); + assert!(res_sum.len() == res_mul.len()); + + self.circuit_stack.push(UnitaryRef::from(Unitary::Not { + input: overflow_qubit_mul.clone(), + })); + + let key_sum = HashableQubitRef::from(overflow_qubit_sum.clone()); + let key_mul = HashableQubitRef::from(overflow_qubit_mul.clone()); + if key_sum != key_mul { + self.circuit_stack.push(UnitaryRef::from(Unitary::Not { + input: overflow_qubit_sum.clone(), + })); + } + let target = self.get_rom(None); + let (value_, controls) = prepare_controls_for_mcx( + &[overflow_qubit_sum.clone(), overflow_qubit_mul.clone()], + &target, + ); + + if let Some(value) = value_ { + if !value { + panic!("overflow constraints are never met!!!"); + } + } else { + assert!(self.is_qubit_rom(&target)); + self.insert_into_constraints(&target, true); + self.circuit_stack + .push(UnitaryRef::from(Unitary::Mcx { controls, target })); + } + + self.circuit_stack.push(UnitaryRef::from(Unitary::Not { + input: overflow_qubit_mul, + })); + if key_sum != key_mul { + self.circuit_stack.push(UnitaryRef::from(Unitary::Not { + input: overflow_qubit_sum, + })); + } + } + + assert!(c.len() == r.len()); + assert!(c.len() == right_operand.len()); + let c_answer = c[..(sort - 1)].to_vec(); + let r_answer = r[..(sort - 1)].to_vec(); + assert!(c_answer.len() == r_answer.len()); + assert!(self.is_rom(&c_answer)); + assert!(self.is_rom(&r_answer)); + self.uncompute(&gates_to_uncompute); + (c_answer, r_answer) + } + } + + pub fn _get_value_from_nid( + &self, + nid: Nid, + assignments: &HashMap, + ) -> Option { + let node = self.mapping_nids.get(&nid).unwrap(); + let node_hash = HashableNodeRef::from(node.clone()); + self.current_state_nodes.get(&node_hash)?; + let index = self.current_state_nodes.get(&node_hash).unwrap(); + + let replacements = self.mapping.get(&node_hash).unwrap(); + + let qubits = replacements[index].clone(); + let mut current_power = 1; + + let mut answer = 0; + for qubit in qubits { + let key = HashableQubitRef::from(qubit.clone()); + if let Some(value) = assignments.get(&key) { + answer += (*value as i64) * current_power; + } else if let Some(v) = get_constant(&qubit.clone()) { + answer += (v as i64) * current_power; + } else { + return None; + } + current_power <<= 1; + } + Some(answer) + } + + fn print_stats(&self) { + let mut count_gates = 0; + let mut count_multiqubit_gates = 0; + let mut count_single_qubit_gates = 0; + let mut count_qubits = 2; // For qubit const false, and const true + let mut max_mcx_length = 0; + + let mut qubits_used: HashSet = HashSet::new(); + + for gate in self.circuit_stack.iter() { + match &*gate.borrow() { + Unitary::Not { input } => { + count_gates += 1; + if !is_constant(input) { + let key = HashableQubitRef::from(input.clone()); + if !qubits_used.contains(&key) { + count_qubits += 1; + qubits_used.insert(key); + } + } + + count_single_qubit_gates += 1; + } + Unitary::Cnot { control, target } => { + count_gates += 1; + if !is_constant(control) { + let key_control = HashableQubitRef::from(control.clone()); + + if !qubits_used.contains(&key_control) { + count_qubits += 1; + qubits_used.insert(key_control); + } + } + + if !is_constant(target) { + let key_target = HashableQubitRef::from(target.clone()); + if !qubits_used.contains(&key_target) { + count_qubits += 1; + qubits_used.insert(key_target); + } + } + max_mcx_length = max(max_mcx_length, 1); + count_multiqubit_gates += 1; + } + Unitary::Mcx { controls, target } => { + count_gates += 1; + max_mcx_length = max(max_mcx_length, controls.len()); + for control in controls.iter() { + if !is_constant(control) { + let key_control = HashableQubitRef::from(control.clone()); + + if !qubits_used.contains(&key_control) { + count_qubits += 1; + qubits_used.insert(key_control); + } + } + } + + if !is_constant(target) { + let key_target = HashableQubitRef::from(target.clone()); + if !qubits_used.contains(&key_target) { + count_qubits += 1; + qubits_used.insert(key_target); + } + } + + count_multiqubit_gates += 1; + } + _ => {} + } + } + + println!("******* QUANTUM CIRCUIT STATS ********"); + println!("Qubits required: {}", count_qubits); + println!("Total gates: {}", count_gates); + println!("Single-qubit gates: {}", count_single_qubit_gates); + println!("MCX gates: {}", count_multiqubit_gates); + println!("Max. controls in MCX: {}", max_mcx_length); + println!("**************************************"); + } + + fn ult( + &mut self, + left: &[QubitRef], + right: &[QubitRef], + is_division: &bool, + gates_to_uncompute: &mut Vec, + is_rom: bool, + ) -> Vec { + let mut left_operand = left.to_owned(); + let mut right_operand = right.to_owned(); + if !is_division { + left_operand.push(QubitRef::from(Qubit::ConstFalse)); + right_operand.push(QubitRef::from(Qubit::ConstFalse)); + } + self.sub(&left_operand, &right_operand, gates_to_uncompute, is_rom) + } + + fn process(&mut self, node: &NodeRef) -> Vec { + if let Some(replacement) = self.get_last_qubitset(node) { + return replacement; + } + self.mapping_nids.insert(get_nid(node), node.clone()); + match &*node.borrow() { + Node::Const { sort, imm, .. } => { + let replacement = get_replacement_from_constant(sort, *imm); + assert!(replacement.len() == sort.bitsize()); + assert!(self.is_rom(&replacement)); + self.record_mapping(node, 0, replacement) + } + Node::State { + init: None, + sort, + name, + .. + } => { + // this is an input + let name = name.as_deref().unwrap_or("?"); + self.process_input(sort.bitsize(), node, name.to_string()) + } + Node::Input { sort, name, .. } => { + self.process_input(sort.bitsize(), node, name.to_string()) + } + Node::State { sort, init, .. } => { + // This is a normal state + let mut replacement = Vec::new(); + if let Some(value) = init { + replacement = self.process(value); + } else { + for _ in 0..sort.bitsize() { + replacement.push(QubitRef::from(Qubit::ConstFalse)); + } + } + assert!(replacement.len() == sort.bitsize()); + assert!(self.is_rom(&replacement)); + self.record_mapping(node, 0, replacement) + } + Node::Not { value, .. } => { + let mut bitvector = self.process(value); + assert!(self.is_rom(&bitvector)); + let mut replacement: Vec = Vec::new(); + for bit in bitvector.iter_mut() { + replacement.push(self.not_gate(bit)); + } + assert!(replacement.len() == bitvector.len()); + assert!(self.is_rom(&replacement)); + self.record_mapping(node, self.current_n, replacement) + } + Node::Bad { cond, nid, .. } => { + self.circuit_stack.push(UnitaryRef::from(Unitary::Barrier)); + let replacement = self.process(cond); + assert!(replacement.len() == 1); + if get_constant(&replacement[0]).is_none() { + let key = HashableQubitRef::from(replacement[0].clone()); + self.qubit_to_nid.insert(key, *nid); + } + assert!(self.is_rom(&replacement)); + self.record_mapping(node, self.current_n, replacement) + } + Node::And { left, right, .. } => { + let left_operand = self.process(left); + let right_operand = self.process(right); + assert!(self.is_rom(&left_operand)); + assert!(self.is_rom(&right_operand)); + let mut replacement: Vec = vec![]; + assert!(left_operand.len() == right_operand.len()); + let mut gates_to_uncompute = Vec::new(); + for (l_qubit, r_qubit) in left_operand.iter().zip(right_operand.iter()) { + let const_l = get_constant(l_qubit); + let const_r = get_constant(r_qubit); + if are_both_constants(const_l, const_r) { + let val = const_l.unwrap() && const_r.unwrap(); + replacement.push(get_qubit_from_bool(val)); + } else if are_there_false_constants(vec![const_r, const_l]) { + replacement.push(QubitRef::from(Qubit::ConstFalse)); + } else if are_there_true_constants(vec![const_l, const_r]) { + let control: QubitRef = if is_constant(l_qubit) { + // l_qubit must be true + r_qubit.clone() + } else { + // const_r must be true + l_qubit.clone() + }; + + let target: QubitRef = self.apply_mcx_gate( + &mut [control], + &None, + &mut gates_to_uncompute, + true, + true, + ); + replacement.push(target); + } else { + // there are no constants + let target = self.apply_mcx_gate( + &mut [l_qubit.clone(), r_qubit.clone()], + &None, + &mut gates_to_uncompute, + true, + true, + ); + + assert!(gates_to_uncompute.is_empty()); + replacement.push(target); + } + } + assert!(replacement.len() == left_operand.len()); + assert!(gates_to_uncompute.is_empty()); + assert!(self.is_rom(&replacement)); + self.record_mapping(node, self.current_n, replacement) + } + Node::Ext { from, value, .. } => { + let mut replacement: Vec = self.process(value); + assert!(replacement.len() == from.bitsize()); + for _ in 0..(self.word_size - from.bitsize()) { + replacement.push(QubitRef::from(Qubit::ConstFalse)); + } + assert!(self.is_rom(&replacement)); + self.record_mapping(node, self.current_n, replacement) + } + Node::Eq { left, right, .. } => { + let left_operand = self.process(left); + let right_operand = self.process(right); + assert!(self.is_rom(&left_operand)); + assert!(self.is_rom(&right_operand)); + let mut gates_to_uncompute = Vec::new(); + let mut replacement = self.eq( + &left_operand, + &right_operand, + &mut gates_to_uncompute, + true, + true, + ); + assert!(self.is_rom(&replacement)); + replacement = self.get_safe_uncomputable_rom(&gates_to_uncompute, &replacement); + self.uncompute(&gates_to_uncompute); + // assert!(self.used_ancillas.is_empty()); + + self.record_mapping(node, self.current_n, replacement) + } + Node::Add { left, right, .. } => { + let left_operand = self.process(left); + let right_operand = self.process(right); + assert!(self.is_rom(&left_operand)); + assert!(self.is_rom(&right_operand)); + + let mut gates_to_uncompute = Vec::new(); + let replacement = + self.add(&left_operand, &right_operand, &mut gates_to_uncompute, true); + self.uncompute(&gates_to_uncompute); + assert!(self.is_rom(&replacement)); + // assert!(self.used_ancillas.is_empty()); + self.record_mapping(node, self.current_n, replacement) + } + Node::Ite { + cond, left, right, .. + } => { + let cond_operand = self.process(cond); + assert!(self.is_rom(&cond_operand)); + assert!(cond_operand.len() == 1); + let mut replacement: Vec; + if let Some(cond_val) = get_constant(&cond_operand[0]) { + if cond_val { + replacement = self.process(left); + assert!(self.is_rom(&replacement)); + } else { + replacement = self.process(right); + assert!(self.is_rom(&replacement)); + } + } else { + let mut gates_to_uncompute = Vec::new(); + replacement = Vec::new(); + let left_operand = self.process(left); + let right_operand = self.process(right); + assert!(self.is_rom(&left_operand)); + assert!(self.is_rom(&right_operand)); + for (_i, (l_qubit, r_qubit)) in + left_operand.iter().zip(right_operand.iter()).enumerate() + { + let const_l = get_constant(l_qubit); + let const_r = get_constant(r_qubit); + + if are_both_constants(const_l, const_r) { + if const_l.unwrap() == const_r.unwrap() { + replacement.push(l_qubit.clone()); + } else if const_l.unwrap() { + // true-part is true + replacement.push(cond_operand[0].clone()); + } else { + // true-part is false and false-part is true + let mut target = self.apply_mcx_gate( + &mut [cond_operand[0].clone()], + &None, + &mut gates_to_uncompute, + true, + false, + ); + target = self.add_not_gate(&mut target, None); + replacement.push(target.clone()); + } + } else if are_there_false_constants(vec![const_l, const_r]) { + let target: QubitRef = if is_constant(l_qubit) { + assert!(!is_constant(&cond_operand[0])); + assert!(!is_constant(r_qubit)); + + self.add_not_gate(&mut cond_operand[0].clone(), None); + let t = self.apply_mcx_gate( + &mut [cond_operand[0].clone(), r_qubit.clone()], + &None, + &mut gates_to_uncompute, + true, + false, + ); + self.add_not_gate(&mut cond_operand[0].clone(), None); + t + } else { + assert!(!is_constant(&cond_operand[0])); + assert!(!is_constant(l_qubit)); + self.apply_mcx_gate( + &mut [cond_operand[0].clone(), l_qubit.clone()], + &None, + &mut gates_to_uncompute, + true, + true, + ) + }; + replacement.push(target); + } else { + // TODO: Optimize when there is only one constant and its true? + assert!(!is_constant(&cond_operand[0])); + + // no constants + let mut target: QubitRef = self.apply_mcx_gate( + &mut [cond_operand[0].clone(), l_qubit.clone()], + &None, + &mut gates_to_uncompute, + true, + false, + ); + + self.add_not_gate(&mut cond_operand[0].clone(), None); + + target = self.apply_mcx_gate( + &mut [cond_operand[0].clone(), r_qubit.clone()], + &Some(target), + &mut gates_to_uncompute, + true, + false, + ); + + self.add_not_gate(&mut cond_operand[0].clone(), None); + replacement.push(target.clone()); + } + } + assert!(replacement.len() == left_operand.len()); + assert!(gates_to_uncompute.is_empty()); + } + assert!(self.is_rom(&replacement)); + self.record_mapping(node, self.current_n, replacement) + } + Node::Sub { left, right, .. } => { + let left_operand = self.process(left); + let right_operand = self.process(right); + assert!(self.is_rom(&left_operand)); + assert!(self.is_rom(&right_operand)); + let mut gates_to_uncompute = Vec::new(); + let replacement = + self.sub(&left_operand, &right_operand, &mut gates_to_uncompute, true); + self.uncompute(&gates_to_uncompute); + // assert!(self.used_ancillas.is_empty()); + assert!(self.is_rom(&replacement)); + self.record_mapping(node, self.current_n, replacement) + } + Node::Ult { left, right, .. } => { + let left_operand = self.process(left); + let right_operand = self.process(right); + assert!(left_operand.len() == right_operand.len()); + assert!(self.is_rom(&left_operand)); + assert!(self.is_rom(&right_operand)); + let mut gates_to_uncompute = Vec::new(); + let result = self.ult( + &left_operand, + &right_operand, + &false, + &mut gates_to_uncompute, + true, + ); + assert!(result.len() == left_operand.len() + 1); + let replacement = vec![result[result.len() - 1].clone()]; + assert!(self.is_rom(&replacement)); + self.uncompute(&gates_to_uncompute); + // assert!(self.used_ancillas.is_empty()); + self.record_mapping(node, self.current_n, replacement) + } + Node::Mul { left, right, .. } => { + let left_operand = self.process(left); + let right_operand = self.process(right); + assert!(self.is_rom(&left_operand)); + assert!(self.is_rom(&right_operand)); + let mut gates_to_uncompute = Vec::new(); + let mut replacement = + self.mul(&left_operand, &right_operand, &mut gates_to_uncompute, true); + assert!(self.is_rom(&replacement)); + replacement = self.get_safe_uncomputable_rom(&gates_to_uncompute, &replacement); + self.uncompute(&gates_to_uncompute); + // assert!(self.used_ancillas.is_empty()); + self.record_mapping(node, self.current_n, replacement) + } + Node::Divu { + left, right, nid, .. + } => { + let (replacement, _) = self.div(left, right, nid); + self.record_mapping(node, self.current_n, replacement) + } + Node::Rem { + left, right, nid, .. + } => { + let (_, replacement) = self.div(left, right, nid); + self.record_mapping(node, self.current_n, replacement) + } + Node::Next { state, next, .. } => { + let _ = self.process(state); + self.circuit_stack.push(UnitaryRef::from(Unitary::Barrier)); + let replacement = self.process(next); + assert!(self.is_rom(&replacement)); + self.record_mapping(state, self.current_n, replacement) + // } + } + Node::Read { .. } | Node::Write { .. } => { + unimplemented!() + } + _ => { + panic!("Unknown BTOR2 node!"); + } + } + } + + pub fn process_model(&mut self, unroll_depth: usize) -> Result<()> { + assert!(self.bad_state_qubits.is_empty()); + assert!(self.bad_state_nodes.is_empty()); + assert!(self.input_qubits.is_empty()); + assert!(self.circuit_stack.is_empty()); + assert!(self.word_size == 64 || self.word_size == 32); + for i in 1..(unroll_depth + 1) { + self.current_n = i as i32; + for sequential in &self.model.sequentials { + if let Node::Next { .. } = &*sequential.borrow() { + let _ = self.process(sequential); + } else { + panic!("expecting 'Next' node here"); + } + } + for bad_state in &self.model.bad_states_initial { + let bitblasted_bad_state = self.process(bad_state); + assert!(bitblasted_bad_state.len() == 1); + if let Some(val) = get_constant(&bitblasted_bad_state[0]) { + if val { + println!( + "Bad state found at state transition {} ({})", + i, + get_nid(bad_state) + ); + self.result_ored_bad_states = QubitRef::from(Qubit::ConstTrue); + break; + } + } else { + self.bad_state_qubits.push(bitblasted_bad_state[0].clone()); + } + } + + for bad_state in &self.model.bad_states_sequential { + let bitblasted_bad_state = self.process(bad_state); + assert!(bitblasted_bad_state.len() == 1); + if let Some(val) = get_constant(&bitblasted_bad_state[0]) { + if val { + println!( + "Bad state found at state transition {} ({})", + i, + get_nid(bad_state) + ); + self.result_ored_bad_states = QubitRef::from(Qubit::ConstTrue); + break; + } + } else { + self.bad_state_qubits.push(bitblasted_bad_state[0].clone()); + } + } + } + + if self.bad_state_qubits.is_empty() && !is_constant(&self.result_ored_bad_states) { + self.result_ored_bad_states = QubitRef::from(Qubit::ConstFalse); + } + + if !is_constant(&self.result_ored_bad_states) { + let (val, bad_state_qubits) = + prepare_controls_for_mcx(&self.bad_state_qubits, &self.result_ored_bad_states); + + if let Some(v) = val { + self.result_ored_bad_states = get_qubit_from_bool(v); + } else if bad_state_qubits.is_empty() { + self.result_ored_bad_states = QubitRef::from(Qubit::ConstFalse); + self.output_oracle = Some(QubitRef::from(Qubit::ConstFalse)); + } else if bad_state_qubits.len() == 1 { + self.result_ored_bad_states = self.bad_state_qubits[0].clone(); + } else { + let temp_ored = self.result_ored_bad_states.clone(); + self.or_bad_state_qubits(bad_state_qubits, &temp_ored); + } + } else { + println!( + "OR of bad states has a constant value -> {}", + get_constant(&self.result_ored_bad_states).unwrap() + ); + } + + if self.constraints.is_empty() { + self.output_oracle = Some(self.result_ored_bad_states.clone()); + } else if self.output_oracle.is_none() { + let mut tmp_controls: Vec = vec![]; + + if let Some(val_ored_bad_states) = get_constant(&self.result_ored_bad_states) { + assert!(val_ored_bad_states); + } else { + tmp_controls.push(self.result_ored_bad_states.clone()); + } + for (key, value) in self.constraints.iter() { + let qubit = &key.value; + tmp_controls.push(qubit.clone()); + if !value { + if let Some(q_val) = get_constant(qubit) { + if q_val { + println!("the constraints are never met"); + } + } else { + self.circuit_stack.push(UnitaryRef::from(Unitary::Not { + input: qubit.clone(), + })); + } + } + } + let target = self.get_rom(None); + let (val_oracle, controls) = prepare_controls_for_mcx(&tmp_controls, &target); + if let Some(value) = val_oracle { + self.output_oracle = Some(get_qubit_from_bool(value)); + if value { + println!("This oracle always evaluate to -> {}", value); + } + } else { + self.circuit_stack.push(UnitaryRef::from(Unitary::Mcx { + controls, + target: target.clone(), + })); + self.output_oracle = Some(target); + } + } + self.print_stats(); + Ok(()) + } + + pub fn _write_model(&self, mut _out: W) -> Result<()> + where + W: Write, + { + println!("missing implementation to write model"); + Ok(()) + } + + pub fn _dump_assignments(&self, assignment: &HashMap) -> Result<()> { + let mut file = File::create("assignments.txt")?; + file.write_all(b"nid,value\n")?; + for (nid, _) in self.mapping_nids.iter() { + if let Some(value) = self._get_value_from_nid(*nid, assignment) { + let line = format!("{},{}\n", nid, value); + file.write_all(line.as_bytes())?; + } + } + Ok(()) + } +} + +#[cfg(test)] +mod tests { + use crate::unicorn::builder::generate_model; + use crate::unicorn::memory::replace_memory; + use bytesize::ByteSize; + use riscu::load_object_file; + use std::path::Path; + + use super::*; + use crate::unicorn::btor2file_parser::parse_btor2_file; + + #[test] + fn test_constants_funcs() { + assert!(matches!( + &*get_qubit_from_constant_bit(1).borrow(), + Qubit::ConstTrue + )); + assert!(matches!( + &*get_qubit_from_constant_bit(0).borrow(), + Qubit::ConstFalse + )); + assert!(matches!( + &*get_qubit_from_bool(true).borrow(), + Qubit::ConstTrue + )); + assert!(matches!( + &*get_qubit_from_bool(false).borrow(), + Qubit::ConstFalse + )); + + assert!(is_constant(&QubitRef::from(Qubit::ConstFalse))); + + assert!(is_constant(&QubitRef::from(Qubit::ConstTrue))); + + assert!(!is_constant(&QubitRef::from(Qubit::QBit { + name: "some_name".to_string(), + dependency: None, + stack: VecDeque::new() + }))); + + assert!(get_constant(&QubitRef::from(Qubit::ConstTrue)).unwrap()); + + assert!(!get_constant(&QubitRef::from(Qubit::ConstFalse)).unwrap()); + assert!(get_constant(&QubitRef::from(Qubit::QBit { + name: "some_name".to_string(), + dependency: None, + stack: VecDeque::new() + })) + .is_none()); + + assert!(are_both_constants(Some(true), Some(false))); + assert!(are_both_constants(Some(true), Some(true))); + assert!(are_both_constants(Some(false), Some(true))); + assert!(are_both_constants(Some(false), Some(false))); + assert!(!are_both_constants(None, Some(false))); + assert!(!are_both_constants(None, None)); + assert!(!are_both_constants(Some(false), None)); + + assert!(!are_there_false_constants(vec![])); + assert!(!are_there_false_constants(vec![Some(true)])); + assert!(!are_there_false_constants(vec![None, None])); + assert!(are_there_false_constants(vec![Some(false)])); + + assert!(!are_there_true_constants(vec![])); + assert!(are_there_true_constants(vec![Some(true)])); + assert!(!are_there_true_constants(vec![None, None])); + assert!(!are_there_true_constants(vec![Some(false)])); + + let sort = NodeType::Bit; + let value = 1; + let bitsize = sort.bitsize(); + assert!(bitsize == 1); + + let replacement = get_replacement_from_constant(&sort, value); + assert!(value == 1); + assert!(replacement.len() == bitsize); + assert!(matches!(&*replacement[0].borrow(), Qubit::ConstTrue)); + } + + #[test] + fn test_prepare_controls_for_mcx() { + let supers_qubit1 = QubitRef::from(Qubit::QBit { + name: "qubit1".to_string(), + dependency: None, + stack: VecDeque::new(), + }); + + let supers_qubit2 = QubitRef::from(Qubit::QBit { + name: "qubit2".to_string(), + dependency: None, + stack: VecDeque::new(), + }); + + let const_false = QubitRef::from(Qubit::ConstFalse); + + let const_true = QubitRef::from(Qubit::ConstTrue); + + let (value, controls) = + prepare_controls_for_mcx(&[const_false, supers_qubit1.clone()], &supers_qubit2); + + assert!(!value.unwrap()); + assert!(controls.is_empty()); + + let (value2, controls2) = + prepare_controls_for_mcx(&[const_true.clone(), const_true], &supers_qubit1); + + assert!(value2.unwrap()); + assert!(controls2.is_empty()); + + let (value3, controls3) = + prepare_controls_for_mcx(&[supers_qubit1.clone()], &supers_qubit1); + + assert!(value3.is_none()); + assert!(controls3.len() == 1); + } + + #[test] + fn eq_test() { + let model = parse_btor2_file(Path::new("examples/quarc/eq.btor2")); + // assert!(model.bad_states_initial.len() == 1); + assert!(model.sequentials.is_empty()); + + let mut qc = QuantumCircuit::new(&model, 64); + + let _ = qc.process_model(1); + assert!(qc.input_qubits.len() == 2); + + assert!( + evaluate_input( + &[0, 0], + &qc.output_oracle, + &qc.input_qubits, + &qc.circuit_stack, + &qc.dependencies + ) + .0 + ); + assert!( + evaluate_input( + &[1, 1], + &qc.output_oracle, + &qc.input_qubits, + &qc.circuit_stack, + &qc.dependencies + ) + .0 + ); + assert!( + !evaluate_input( + &[0, 1], + &qc.output_oracle, + &qc.input_qubits, + &qc.circuit_stack, + &qc.dependencies + ) + .0 + ); + assert!( + !evaluate_input( + &[1, 0], + &qc.output_oracle, + &qc.input_qubits, + &qc.circuit_stack, + &qc.dependencies + ) + .0 + ); + } + + #[test] + fn eq8_test() { + let model = parse_btor2_file(Path::new("examples/quarc/eq8.btor2")); + // // assert!(model.bad_states_initial.len() == 1); + assert!(model.sequentials.is_empty()); + let mut qc = QuantumCircuit::new(&model, 64); + let _ = qc.process_model(1); + assert!(qc.input_qubits.len() == 2); + + for i in 0..256 { + for j in 0..256 { + if i == j { + assert!( + evaluate_input( + &[i, j], + &qc.output_oracle, + &qc.input_qubits, + &qc.circuit_stack, + &qc.dependencies + ) + .0 + ); + } else { + assert!( + !evaluate_input( + &[i, j], + &qc.output_oracle, + &qc.input_qubits, + &qc.circuit_stack, + &qc.dependencies + ) + .0 + ); + } + } + } + } + + #[test] + fn eq82_test() { + let model = parse_btor2_file(Path::new("examples/quarc/eq82.btor2")); + // // assert!(model.bad_states_initial.len() == 1); + assert!(model.sequentials.is_empty()); + let mut qc = QuantumCircuit::new(&model, 64); + let _ = qc.process_model(1); + assert!(qc.input_qubits.len() == 1); + + for i in 0..256 { + if i == 0 { + assert!( + evaluate_input( + &[i], + &qc.output_oracle, + &qc.input_qubits, + &qc.circuit_stack, + &qc.dependencies + ) + .0 + ); + } else { + assert!( + !evaluate_input( + &[i], + &qc.output_oracle, + &qc.input_qubits, + &qc.circuit_stack, + &qc.dependencies + ) + .0 + ); + } + } + } + + #[test] + fn ult2_test() { + let model = parse_btor2_file(Path::new("examples/quarc/ult2.btor2")); + // assert!(model.bad_states_initial.len() == 1); + assert!(model.sequentials.is_empty()); + let mut qc = QuantumCircuit::new(&model, 64); + let _ = qc.process_model(1); + assert!(qc.input_qubits.len() == 1); + + for i in 0..256 { + if i < 213 { + assert!( + evaluate_input( + &[i], + &qc.output_oracle, + &qc.input_qubits, + &qc.circuit_stack, + &qc.dependencies + ) + .0 + ); + } else { + assert!( + !evaluate_input( + &[i], + &qc.output_oracle, + &qc.input_qubits, + &qc.circuit_stack, + &qc.dependencies + ) + .0 + ); + } + } + } + + #[test] + fn add_test() { + let model = parse_btor2_file(Path::new("examples/quarc/add.btor2")); + // assert!(model.bad_states_initial.len() == 1); + assert!(model.sequentials.len() == 1); + let mut qc = QuantumCircuit::new(&model, 64); + let _ = qc.process_model(1); + assert!(qc.input_qubits.len() == 2); + + for i in 0..256 { + for j in 0..256 { + let result = (i + j) & 255; + + let (oracle_val, assignments) = evaluate_input( + &[i, j], + &qc.output_oracle, + &qc.input_qubits, + &qc.circuit_stack, + &qc.dependencies, + ); + assert!(oracle_val); + + let circuit_value = qc._get_value_from_nid(4, &assignments); + assert!(circuit_value.is_some()); + assert!(result == circuit_value.unwrap()); + } + } + } + + #[test] + fn add2_test() { + let model = parse_btor2_file(Path::new("examples/quarc/add2.btor2")); + // // assert!(model.bad_states_initial.len() == 1); + assert!(model.sequentials.len() == 1); + let mut qc = QuantumCircuit::new(&model, 64); + let _ = qc.process_model(1); + assert!(qc.input_qubits.len() == 1); + + for i in 0..256 { + let result = (i + 10) & 255; + + let (oracle_val, assignments) = evaluate_input( + &[i], + &qc.output_oracle, + &qc.input_qubits, + &qc.circuit_stack, + &qc.dependencies, + ); + assert!(oracle_val); + + let circuit_value = qc._get_value_from_nid(4, &assignments); + assert!(circuit_value.is_some()); + assert!(result == circuit_value.unwrap()); + } + } + + #[test] + fn sub2_test() { + let model = parse_btor2_file(Path::new("examples/quarc/sub2.btor2")); + assert!(model.sequentials.len() == 1); + let mut qc = QuantumCircuit::new(&model, 64); + let _ = qc.process_model(1); + assert!(qc.input_qubits.len() == 1); + + for i in 0..256 { + let result = (255 - i) & 255; + + let (_oracle_val, assignments) = evaluate_input( + &[i], + &qc.output_oracle, + &qc.input_qubits, + &qc.circuit_stack, + &qc.dependencies, + ); + // assert!(oracle_val); + + let circuit_value = qc._get_value_from_nid(4, &assignments); + assert!(circuit_value.is_some()); + println!("{} {} {}", i, result, circuit_value.unwrap()); + assert!(result == circuit_value.unwrap()); + } + } + + #[test] + fn and_test() { + let model = parse_btor2_file(Path::new("examples/quarc/and.btor2")); + // assert!(model.bad_states_initial.len() == 1); + assert!(model.sequentials.len() == 1); + let mut qc = QuantumCircuit::new(&model, 64); + let _ = qc.process_model(1); + assert!(qc.input_qubits.len() == 2); + + for i in 0..256 { + for j in 0..256 { + let result = i & j & 255; + + let (oracle_val, assignments) = evaluate_input( + &[i, j], + &qc.output_oracle, + &qc.input_qubits, + &qc.circuit_stack, + &qc.dependencies, + ); + assert!(oracle_val); + let circuit_value = qc._get_value_from_nid(4, &assignments); + assert!(circuit_value.is_some()); + assert!(result == circuit_value.unwrap()); + } + } + } + + #[test] + fn and2_test() { + let model = parse_btor2_file(Path::new("examples/quarc/and2.btor2")); + // assert!(model.bad_states_initial.len() == 1); + assert!(model.sequentials.len() == 1); + let mut qc = QuantumCircuit::new(&model, 64); + let _ = qc.process_model(1); + assert!(qc.input_qubits.len() == 1); + + for i in 0..256 { + let result = i & 241 & 255; + + let (oracle_val, assignments) = evaluate_input( + &[i], + &qc.output_oracle, + &qc.input_qubits, + &qc.circuit_stack, + &qc.dependencies, + ); + assert!(oracle_val); + let circuit_value = qc._get_value_from_nid(4, &assignments); + assert!(circuit_value.is_some()); + println!("{} {}", i, circuit_value.unwrap()); + assert!(result == circuit_value.unwrap()); + } + } + + #[test] + fn twos_complement_test() { + let model = parse_btor2_file(Path::new("examples/quarc/sub.btor2")); + let mut qc = QuantumCircuit::new(&model, 64); + + let mut assignments: HashMap = HashMap::new(); + let mut const_qubitset: Vec = vec![]; + for i in 0..8 { + const_qubitset.push(QubitRef::from(Qubit::QBit { + name: "temp".to_string(), + dependency: None, + stack: VecDeque::new(), + })); + let key = HashableQubitRef::from(const_qubitset[i].clone()); + assignments.insert(key, false); + } + const_qubitset.push(QubitRef::from(Qubit::ConstFalse)); + + let (_gates, answer) = qc.twos_complement(&const_qubitset); + evaluate_circuit(&mut assignments, &qc.circuit_stack, &qc.dependencies); + + for item in answer.iter().take(9) { + let key = HashableQubitRef::from(item.clone()); + let value = assignments.get(&key).unwrap(); + assert!(!value); + } + } + + #[test] + fn test_const_add() { + let model = parse_btor2_file(Path::new("examples/quarc/add.btor2")); + let mut qc = QuantumCircuit::new(&model, 64); + let mut gates_to_uncompute = Vec::new(); + let wordsize = 9; + for i in 1..256 { + for j in 0..256 { + let result: i32 = (i + j) & (256 * 2 - 1); + + let left_operand = get_qubitset_from_constant(&(i as u64), &wordsize); + let right_operand = get_qubitset_from_constant(&(j as u64), &wordsize); + + let res_qubitset = + qc.add(&left_operand, &right_operand, &mut gates_to_uncompute, true); + + let mut local_result = 0; + let mut curr_power = 1; + for qubit in res_qubitset.iter() { + if let Some(v) = get_constant(qubit) { + if v { + local_result += curr_power; + } + } else { + unreachable!(); + } + curr_power <<= 1; + } + assert!(local_result == result); + } + } + } + + #[test] + fn test_const_sub() { + let model = parse_btor2_file(Path::new("examples/quarc/sub.btor2")); + let mut qc = QuantumCircuit::new(&model, 64); + + let wordsize = 9; + for i in 0..256 { + for j in 0..256 { + let result: i32 = (i - j) & 511; + + let left_operand = get_qubitset_from_constant(&(i as u64), &wordsize); + let right_operand = get_qubitset_from_constant(&(j as u64), &wordsize); + + let mut gates_to_uncompute = Vec::new(); + let res_qubitset = + qc.sub(&left_operand, &right_operand, &mut gates_to_uncompute, true); + + let mut local_result = 0; + let mut curr_power = 1; + for qubit in res_qubitset.iter() { + if let Some(v) = get_constant(qubit) { + if v { + local_result += curr_power; + } + } else { + unreachable!() + } + curr_power <<= 1; + } + // println!("{}-{}= {}, got {}.", i, j, result, local_result); + assert!(local_result == result); + } + } + } + + #[test] + fn sub_test() { + let model = parse_btor2_file(Path::new("examples/quarc/sub.btor2")); + // assert!(model.bad_states_initial.len() == 1); + assert!(model.sequentials.len() == 1); + let mut qc = QuantumCircuit::new(&model, 64); + let _ = qc.process_model(1); + assert!(qc.input_qubits.len() == 2); + + for i in 0..256 { + for j in 0..256 { + let result = (i - j) & 255; + + let (oracle_val, assignments) = evaluate_input( + &[i, j], + &qc.output_oracle, + &qc.input_qubits, + &qc.circuit_stack, + &qc.dependencies, + ); + assert!(oracle_val); + + let circuit_value = qc._get_value_from_nid(4, &assignments); + assert!(circuit_value.is_some()); + assert!(result == circuit_value.unwrap()); + } + } + } + + #[test] + fn test_const_ult() { + let model = parse_btor2_file(Path::new("examples/quarc/add.btor2")); + let mut qc = QuantumCircuit::new(&model, 64); + + let wordsize = 8; + let mut gates_to_uncompute = Vec::new(); + for i in 1..256 { + for j in 0..256 { + let result: bool = i < j; + + let left_operand = get_qubitset_from_constant(&(i as u64), &wordsize); + let right_operand = get_qubitset_from_constant(&(j as u64), &wordsize); + + let res_qubitset = qc.ult( + &left_operand, + &right_operand, + &false, + &mut gates_to_uncompute, + true, + ); + let ult_result = res_qubitset[res_qubitset.len() - 1].clone(); + // println!( + // "{}<{}={}, got {}.", + // i, + // j, + // result, + // get_constant(&ult_result).unwrap() + // ); + assert!(get_constant(&ult_result).unwrap() == result); + } + } + } + + #[test] + fn ult_test() { + let model = parse_btor2_file(Path::new("examples/quarc/ult.btor2")); + // assert!(model.bad_states_initial.len() == 1); + assert!(model.sequentials.is_empty()); + let mut qc = QuantumCircuit::new(&model, 64); + let _ = qc.process_model(1); + assert!(qc.input_qubits.len() == 2); + for i in 0..256 { + for j in 0..256 { + let (oracle_val, _assignments) = evaluate_input( + &[i, j], + &qc.output_oracle, + &qc.input_qubits, + &qc.circuit_stack, + &qc.dependencies, + ); + println!("{} {} -> {}", i, j, oracle_val); + if i < j { + assert!(oracle_val); + } else { + assert!(!oracle_val); + } + } + } + } + + #[test] + fn ite_test() { + let model = parse_btor2_file(Path::new("examples/quarc/ite.btor2")); + // assert!(model.bad_states_initial.len() == 1); + let mut qc = QuantumCircuit::new(&model, 64); + let _ = qc.process_model(1); + assert!(qc.input_qubits.len() == 3); + for cond in 0..2 { + for true_part in 0..256 { + for false_part in 0..256 { + let (_oracle_val, assignments) = evaluate_input( + &[cond, true_part, false_part], + &qc.output_oracle, + &qc.input_qubits, + &qc.circuit_stack, + &qc.dependencies, + ); + let circuit_value = qc._get_value_from_nid(10, &assignments).unwrap(); + if cond == 1 { + assert!(circuit_value == true_part); + } else { + assert!(circuit_value == false_part); + } + } + } + } + } + + #[test] + fn ite2_test() { + let model = parse_btor2_file(Path::new("examples/quarc/ite2.btor2")); + // assert!(model.bad_states_initial.len() == 1); + let mut qc = QuantumCircuit::new(&model, 64); + let _ = qc.process_model(1); + assert!(qc.input_qubits.len() == 2); + for cond in 0..2 { + for i in 0..256 { + let (_, assignments) = evaluate_input( + &[cond, i], + &qc.output_oracle, + &qc.input_qubits, + &qc.circuit_stack, + &qc.dependencies, + ); + let circuit_value = qc._get_value_from_nid(4, &assignments).unwrap(); + if cond == 1 { + assert!(circuit_value == i); + } else { + assert!(circuit_value == 0); + } + } + } + } + + #[test] + fn not_test() { + let model = parse_btor2_file(Path::new("examples/quarc/not.btor2")); + // assert!(model.bad_states_initial.len() == 1); + assert!(model.sequentials.len() == 1); + let mut qc = QuantumCircuit::new(&model, 64); + let _ = qc.process_model(1); + assert!(qc.input_qubits.len() == 1); + + for i in 0..256 { + let result = !i & 255; + + let (oracle_val, assignments) = evaluate_input( + &[i], + &qc.output_oracle, + &qc.input_qubits, + &qc.circuit_stack, + &qc.dependencies, + ); + println!("i: {}", i); + let circuit_value = qc._get_value_from_nid(3, &assignments); + assert!(circuit_value.is_some()); + assert!(result == circuit_value.unwrap()); + assert!(oracle_val); + } + } + + #[test] + fn mul_test() { + let model = parse_btor2_file(Path::new("examples/quarc/mul.btor2")); + // assert!(model.bad_states_initial.len() == 1); + assert!(model.sequentials.len() == 1); + let mut qc = QuantumCircuit::new(&model, 64); + let _ = qc.process_model(1); + assert!(qc.input_qubits.len() == 2); + + for i in 0..256 { + for j in 0..256 { + let result = (i * j) & 255; + + let (oracle_val, assignments) = evaluate_input( + &[i, j], + &qc.output_oracle.clone(), + &qc.input_qubits, + &qc.circuit_stack, + &qc.dependencies, + ); + assert!(oracle_val); + + let circuit_value = qc._get_value_from_nid(4, &assignments); + assert!(circuit_value.is_some()); + assert!(result == circuit_value.unwrap()); + } + } + } + + #[test] + fn mul2_test() { + let model = parse_btor2_file(Path::new("examples/quarc/mul2.btor2")); + // assert!(model.bad_states_initial.len() == 1); + assert!(model.sequentials.len() == 1); + let mut qc = QuantumCircuit::new(&model, 64); + let _ = qc.process_model(1); + assert!(qc.input_qubits.len() == 1); + + for i in 0..256 { + let result = (i * 3) & 255; + + let (oracle_val, assignments) = evaluate_input( + &[i], + &qc.output_oracle, + &qc.input_qubits, + &qc.circuit_stack, + &qc.dependencies, + ); + assert!(oracle_val); + + let circuit_value = qc._get_value_from_nid(4, &assignments); + assert!(circuit_value.is_some()); + // println!("{} {}", i, circuit_value.unwrap()); + println!("{} {}", result, circuit_value.unwrap()); + assert!(result == circuit_value.unwrap()); + } + } + + #[test] + fn div_test() { + let model = parse_btor2_file(Path::new("examples/quarc/div.btor2")); + // assert!(model.bad_states_initial.len() == 1); + assert!(model.sequentials.len() == 1); + let mut qc = QuantumCircuit::new(&model, 64); + let _ = qc.process_model(1); + assert!(qc.input_qubits.len() == 2); + + for i in 0..256 { + for j in 0..256 { + let (oracle_val, assignments) = evaluate_input( + &[i, j], + &qc.output_oracle, + &qc.input_qubits, + &qc.circuit_stack, + &qc.dependencies, + ); + let circuit_value = qc._get_value_from_nid(4, &assignments); + if j != 0 { + let result = (i / j) & 255; + println!("{} {}", i, j); + // println!( + // "{}/{} --> {} = {}, {}", + // i, + // j, + // result, + // circuit_value.unwrap(), + // get_word_value(&qc.temp, &assignments).unwrap() + // ); + assert!(oracle_val); + assert!(circuit_value.is_some()); + assert!(result == circuit_value.unwrap()); + } + } + } + } + + #[test] + fn one_const_div_test() { + let model = parse_btor2_file(Path::new("examples/quarc/div2.btor2")); + // assert!(model.bad_states_initial.len() == 1); + assert!(model.sequentials.len() == 1); + let mut qc = QuantumCircuit::new(&model, 64); + let _ = qc.process_model(1); + assert!(qc.input_qubits.len() == 1); + + for i in 0..256 { + let (oracle_val, assignments) = evaluate_input( + &[i], + &qc.output_oracle, + &qc.input_qubits, + &qc.circuit_stack, + &qc.dependencies, + ); + let circuit_value = qc._get_value_from_nid(4, &assignments); + + if i != 0 { + // println!("rem {}", get_word_value(&qc.temp, &assignments).unwrap()); + let result = (i / 50) & 255; + // println!("{}/50 = {}, got {}", i, result, circuit_value.unwrap()); + assert!(oracle_val); + assert!(circuit_value.is_some()); + assert!(result == circuit_value.unwrap()); + } + // else { + // assert!(!oracle_val) + // } + } + } + + #[test] + fn rem_test() { + let model = parse_btor2_file(Path::new("examples/quarc/rem.btor2")); + // assert!(model.bad_states_initial.len() == 1); + assert!(model.sequentials.len() == 1); + let mut qc = QuantumCircuit::new(&model, 64); + let _ = qc.process_model(1); + assert!(qc.input_qubits.len() == 2); + for i in 0..256 { + for j in 0..256 { + let (oracle_val, assignments) = evaluate_input( + &[i, j], + &qc.output_oracle, + &qc.input_qubits, + &qc.circuit_stack, + &qc.dependencies, + ); + let circuit_value = qc._get_value_from_nid(5, &assignments); + if j != 0 { + let result = (i % j) & 255; + assert!(oracle_val); + assert!(circuit_value.is_some()); + println!("{} {}, {} {}", i, j, result, circuit_value.unwrap()); + assert!(result == circuit_value.unwrap()); + } + } + } + } + + #[test] + fn symbolic_experiments_no_dynamic_mem() -> Result<()> { + let mut simple_assignment_bad_inputs: HashSet = HashSet::new(); + for i in 0..6 { + simple_assignment_bad_inputs.insert(i); + } + for i in 49..256 { + simple_assignment_bad_inputs.insert(i); + } + + let mut all_inputs_bad: HashSet = HashSet::new(); + let mut all_inputs_bad_but_zero: HashSet = HashSet::new(); + for i in 0..256 { + all_inputs_bad.insert(i); + if i > 0 { + all_inputs_bad_but_zero.insert(i); + } + } + let paths_to_timesteps = HashMap::from([ + ("division-by-zero-3-35.m", (86, HashSet::from([48]))), + ("memory-access-fail-1-35.m", (72, all_inputs_bad)), + // ("nested-if-else-1-35.m", (123, HashSet::from([49]))), + // ("nested-if-else-reverse-1-35.m", (122, HashSet::from([49]))), + // ("return-from-loop-1-35.m", (105, HashSet::from([48]))), // + // ( + // "simple-assignment-1-35.m", + // (105, simple_assignment_bad_inputs), + // ), + // ("simple-if-else-1-35.m", (117, HashSet::from([49]))), + // ( + // "simple-if-else-reverse-1-35.m", + // (115, HashSet::from([49])), + // ), + // ( + // "simple-if-without-else-1-35.m", + // (116, HashSet::from([49])), + // ), + ("d.m", (84, all_inputs_bad_but_zero)), + ]); + + for (file_name, data) in paths_to_timesteps.iter() { + println!("current file: {}", *file_name); + let mut path = "examples/selfie/".to_owned(); + path.push_str(file_name); + let program = load_object_file(&path)?; + let mut model = generate_model(&program, ByteSize::mib(1).as_u64(), 8, 120, &[])?; + + replace_memory(&mut model); + let mut qc = QuantumCircuit::new(&model, 64); + let _ = qc.process_model(data.0); + for input_value in 0..256 { + println!("input value {}", input_value); + let mut input_values = vec![]; + for _ in 0..qc.input_qubits.len() { + input_values.push(input_value as i64); + } + let (oracle_val, _) = evaluate_input( + &input_values, + &qc.output_oracle, + &qc.input_qubits, + &qc.circuit_stack, + &qc.dependencies, + ); + if data.1.get(&input_value).is_some() { + // qc._dump_assignments(&assignments)?; + assert!(oracle_val); + } else { + assert!(!oracle_val); + } + } + } + Ok(()) + } +} diff --git a/src/unicorn/qubot.rs b/src/unicorn/qubot.rs index 00dcfc04..e2f30012 100644 --- a/src/unicorn/qubot.rs +++ b/src/unicorn/qubot.rs @@ -767,6 +767,12 @@ pub struct InputEvaluator { pub fixed_qubits: HashMap, } +impl Default for InputEvaluator { + fn default() -> Self { + Self::new() + } +} + impl InputEvaluator { pub fn new() -> Self { Self { diff --git a/src/unicorn/sat_solver.rs b/src/unicorn/sat_solver.rs index 6c97ef2b..e90513d6 100644 --- a/src/unicorn/sat_solver.rs +++ b/src/unicorn/sat_solver.rs @@ -1,116 +1,25 @@ use crate::unicorn::bitblasting::{get_constant, or_gate, Gate, GateModel, GateRef}; use crate::unicorn::{Node, NodeRef}; -use crate::SatType; use anyhow::{anyhow, Result}; use log::{debug, warn}; -// -// Public Interface -// - -#[allow(unused_variables)] -pub fn solve_bad_states( - gate_model: &GateModel, - sat_type: SatType, - terminate_on_bad: bool, - one_query: bool, -) -> Result<()> { - match sat_type { - SatType::None => unreachable!(), - #[cfg(feature = "kissat")] - SatType::Kissat => process_all_bad_states::( - gate_model, - terminate_on_bad, - one_query, - ), - #[cfg(feature = "varisat")] - SatType::Varisat => process_all_bad_states::( - gate_model, - terminate_on_bad, - one_query, - ), - #[cfg(feature = "cadical")] - SatType::Cadical => process_all_bad_states::( - gate_model, - terminate_on_bad, - one_query, - ), - } -} - -// -// Private Implementation -// - #[allow(dead_code)] #[derive(Debug, Eq, PartialEq)] -enum SATSolution { +pub enum SATSolution { Sat, Unsat, Timeout, } -trait SATSolver { +pub trait SATSolver { fn new() -> Self; fn name() -> &'static str; fn prepare(&mut self, gate_model: &GateModel); fn decide(&mut self, gate_model: &GateModel, gate: &GateRef) -> SATSolution; } -fn process_single_bad_state( - solver: &mut S, - gate_model: &GateModel, - bad_state_: Option<&NodeRef>, - gate: &GateRef, - terminate_on_bad: bool, - one_query: bool, -) -> Result<()> { - if !one_query { - let bad_state = bad_state_.unwrap(); - if let Node::Bad { name, .. } = &*bad_state.borrow() { - let solution = solver.decide(gate_model, gate); - match solution { - SATSolution::Sat => { - warn!( - "Bad state '{}' is satisfiable ({})!", - name.as_deref().unwrap_or("?"), - S::name() - ); - if terminate_on_bad { - return Err(anyhow!("Bad state satisfiable")); - } - } - SATSolution::Unsat => { - debug!( - "Bad state '{}' is unsatisfiable ({}).", - name.as_deref().unwrap_or("?"), - S::name() - ); - } - SATSolution::Timeout => unimplemented!(), - } - Ok(()) - } else { - panic!("expecting 'Bad' node here"); - } - } else { - assert!(bad_state_.is_none()); - let solution = solver.decide(gate_model, gate); - match solution { - SATSolution::Sat => { - warn!("At least one bad state evaluates to true ({})", S::name()); - } - SATSolution::Unsat => { - debug!("No bad states occur ({}).", S::name()); - } - SATSolution::Timeout => unimplemented!(), - } - Ok(()) - } -} - #[allow(dead_code)] -fn process_all_bad_states( +pub fn process_all_bad_states( gate_model: &GateModel, terminate_on_bad: bool, one_query: bool, @@ -178,6 +87,62 @@ fn process_all_bad_states( Ok(()) } +// +// Private Implementation +// + +fn process_single_bad_state( + solver: &mut S, + gate_model: &GateModel, + bad_state_: Option<&NodeRef>, + gate: &GateRef, + terminate_on_bad: bool, + one_query: bool, +) -> Result<()> { + if !one_query { + let bad_state = bad_state_.unwrap(); + if let Node::Bad { name, .. } = &*bad_state.borrow() { + let solution = solver.decide(gate_model, gate); + match solution { + SATSolution::Sat => { + warn!( + "Bad state '{}' is satisfiable ({})!", + name.as_deref().unwrap_or("?"), + S::name() + ); + if terminate_on_bad { + return Err(anyhow!("Bad state satisfiable")); + } + } + SATSolution::Unsat => { + debug!( + "Bad state '{}' is unsatisfiable ({}).", + name.as_deref().unwrap_or("?"), + S::name() + ); + } + SATSolution::Timeout => unimplemented!(), + } + Ok(()) + } else { + panic!("expecting 'Bad' node here"); + } + } else { + assert!(bad_state_.is_none()); + let solution = solver.decide(gate_model, gate); + match solution { + SATSolution::Sat => { + warn!("At least one bad state evaluates to true ({})", S::name()); + } + SATSolution::Unsat => { + debug!("No bad states occur ({}).", S::name()); + } + SATSolution::Timeout => unimplemented!(), + } + Ok(()) + } +} + // TODO: Move this module into separate file. #[cfg(feature = "kissat")] pub mod kissat_impl { diff --git a/src/unicorn/smt_solver.rs b/src/unicorn/smt_solver.rs index 3a16637b..0bda9690 100644 --- a/src/unicorn/smt_solver.rs +++ b/src/unicorn/smt_solver.rs @@ -63,485 +63,3 @@ pub mod none_impl { } } } - -// TODO: Move this module into separate file. -#[cfg(feature = "boolector")] -pub mod boolector_impl { - use crate::unicorn::smt_solver::{SMTSolution, SMTSolver}; - use crate::unicorn::{HashableNodeRef, Node, NodeRef, NodeType}; - use boolector_solver::{ - option::{BtorOption, ModelGen, OutputFileFormat}, - Array, Btor, SolverResult, BV, - }; - use log::debug; - use std::collections::HashMap; - use std::rc::Rc; - use std::time::Duration; - - type ArrayRef = Array>; - type BitVectorRef = BV>; - - #[derive(Clone)] - enum BoolectorValue { - BitVector(BitVectorRef), - Array(ArrayRef), - } - - pub struct BoolectorSolver { - solver: Rc, - mapping: HashMap, - } - - impl SMTSolver for BoolectorSolver { - fn name() -> &'static str { - "Boolector" - } - - fn new(timeout: Option) -> Self { - let solver = Rc::new(Btor::new()); - // TODO: Properly configure the below options. - solver.set_opt(BtorOption::ModelGen(ModelGen::All)); - solver.set_opt(BtorOption::Incremental(true)); - solver.set_opt(BtorOption::OutputFileFormat(OutputFileFormat::SMTLIBv2)); - solver.set_opt(BtorOption::SolverTimeout(timeout)); - Self { - solver, - mapping: HashMap::new(), - } - } - - fn is_always_true(&mut self, node: &NodeRef) -> bool { - let bv = self.visit(node).into_bv().not(); - self.solve_impl(bv) == SMTSolution::Unsat - } - - fn is_always_false(&mut self, node: &NodeRef) -> bool { - let bv = self.visit(node).into_bv(); - self.solve_impl(bv) == SMTSolution::Unsat - } - - fn is_always_equal(&mut self, left: &NodeRef, right: &NodeRef) -> bool { - let bv_left = self.visit(left).into_bv(); - let bv_right = self.visit(right).into_bv(); - let bv = bv_left._ne(&bv_right); - self.solve_impl(bv) == SMTSolution::Unsat - } - - fn solve(&mut self, root: &NodeRef) -> SMTSolution { - let bv = self.visit(root).into_bv(); - self.solve_impl(bv.slice(0, 0)) - } - } - - impl BoolectorSolver { - fn solve_impl(&mut self, bv: BitVectorRef) -> SMTSolution { - self.solver.push(1); - bv.assert(); - let solution = match self.solver.sat() { - SolverResult::Sat => SMTSolution::Sat, - SolverResult::Unsat => SMTSolution::Unsat, - SolverResult::Unknown => SMTSolution::Timeout, - }; - self.solver.pop(1); - if solution == SMTSolution::Timeout { - debug!("Query timeout was reached by Boolector"); - } - solution - } - - fn visit(&mut self, node: &NodeRef) -> BoolectorValue { - let key = HashableNodeRef::from(node.clone()); - self.mapping.get(&key).cloned().unwrap_or_else(|| { - let value = self.translate(node); - assert!(!self.mapping.contains_key(&key)); - self.mapping.insert(key, value.clone()); - value - }) - } - - #[rustfmt::skip] - fn translate(&mut self, node: &NodeRef) -> BoolectorValue { - match &*node.borrow() { - Node::Const { sort, imm, .. } => { - let width = sort.bitsize() as u32; - BV::from_u64(self.solver.clone(), *imm, width).into() - } - Node::Read { memory, address, .. } => { - let array_memory = self.visit(memory).into_array(); - let bv_address = self.visit(address).into_bv(); - array_memory.read(&bv_address).into() - } - Node::Write { memory, address, value, .. } => { - let array_memory = self.visit(memory).into_array(); - let bv_address = self.visit(address).into_bv(); - let bv_value = self.visit(value).into_bv(); - array_memory.write(&bv_address, &bv_value).into() - } - Node::Add { left, right, .. } => { - let bv_left = self.visit(left).into_bv(); - let bv_right = self.visit(right).into_bv(); - bv_left.add(&bv_right).into() - } - Node::Sub { left, right, .. } => { - let bv_left = self.visit(left).into_bv(); - let bv_right = self.visit(right).into_bv(); - bv_left.sub(&bv_right).into() - } - Node::Mul { left, right, .. } => { - let bv_left = self.visit(left).into_bv(); - let bv_right = self.visit(right).into_bv(); - bv_left.mul(&bv_right).into() - } - Node::Divu { left, right, .. } => { - let bv_left = self.visit(left).into_bv(); - let bv_right = self.visit(right).into_bv(); - bv_left.udiv(&bv_right).into() - }, - Node::Div { left, right, .. } => { - let bv_left = self.visit(left).into_bv(); - let bv_right = self.visit(right).into_bv(); - bv_left.sdiv(&bv_right).into() - }, - Node::Rem { left, right, .. } => { - let bv_left = self.visit(left).into_bv(); - let bv_right = self.visit(right).into_bv(); - bv_left.urem(&bv_right).into() - } - Node::Sll { left, right, .. } => { - let bv_left = self.visit(left).into_bv(); - let bv_right = self.visit(right).into_bv(); - bv_left.sll(&bv_right).into() - }, - Node::Srl { left, right, .. } => { - let bv_left = self.visit(left).into_bv(); - let bv_right = self.visit(right).into_bv(); - bv_left.srl(&bv_right).into() - }, - Node::Ult { left, right, .. } => { - let bv_left = self.visit(left).into_bv(); - let bv_right = self.visit(right).into_bv(); - bv_left.ult(&bv_right).into() - } - Node::Ext { from, value, .. } => { - let width = from.bitsize() as u32; - let bv_value = self.visit(value).into_bv(); - assert_eq!(bv_value.get_width(), width); - bv_value.uext(64 - width).into() - } - Node::Ite { sort: NodeType::Memory, cond, left, right, .. } => { - let bv_cond = self.visit(cond).into_bv(); - let array_left = self.visit(left).into_array(); - let array_right = self.visit(right).into_array(); - bv_cond.cond_array(&array_left, &array_right).into() - } - Node::Ite { sort, cond, left, right, .. } => { - let width = sort.bitsize() as u32; - let bv_cond = self.visit(cond).into_bv(); - let bv_left = self.visit(left).into_bv(); - let bv_right = self.visit(right).into_bv(); - assert_eq!(bv_left.get_width(), width); - assert_eq!(bv_right.get_width(), width); - bv_cond.cond_bv(&bv_left, &bv_right).into() - } - Node::Eq { left, right, .. } => { - let bv_left = self.visit(left).into_bv(); - let bv_right = self.visit(right).into_bv(); - bv_left._eq(&bv_right).into() - } - Node::And { left, right, .. } => { - let bv_left = self.visit(left).into_bv(); - let bv_right = self.visit(right).into_bv(); - bv_left.and(&bv_right).into() - } - Node::Or { left, right, .. } => { - let bv_left = self.visit(left).into_bv(); - let bv_right = self.visit(right).into_bv(); - bv_left.or(&bv_right).into() - } - Node::Not { value, .. } => { - let bv_value = self.visit(value).into_bv(); - bv_value.not().into() - } - Node::State { sort: NodeType::Memory, name, .. } => { - Array::new(self.solver.clone(), 64, 64, name.as_deref()).into() - } - Node::State { sort, name, .. } => { - let width = sort.bitsize() as u32; - BV::new(self.solver.clone(), width, name.as_deref()).into() - } - Node::Input { sort, name, .. } => { - let width = sort.bitsize() as u32; - BV::new(self.solver.clone(), width, Some(name)).into() - } - Node::Next { .. } => panic!("should be unreachable"), - Node::Bad { cond, .. } => { - self.visit(cond) - }, - Node::Comment(_) => panic!("cannot translate"), - } - } - } - - impl From for BoolectorValue { - fn from(item: BitVectorRef) -> Self { - Self::BitVector(item) - } - } - - impl From for BoolectorValue { - fn from(item: ArrayRef) -> Self { - Self::Array(item) - } - } - - impl BoolectorValue { - fn into_bv(self) -> BitVectorRef { - match self { - BoolectorValue::BitVector(x) => x, - _ => panic!("expected bit-vector"), - } - } - fn into_array(self) -> ArrayRef { - match self { - BoolectorValue::Array(x) => x, - _ => panic!("expected array"), - } - } - } -} - -// TODO: Move this module into separate file. -#[cfg(feature = "z3")] -pub mod z3solver_impl { - use crate::unicorn::smt_solver::{SMTSolution, SMTSolver}; - use crate::unicorn::{HashableNodeRef, Node, NodeRef, NodeType}; - use log::debug; - use std::collections::HashMap; - use std::convert::TryInto; - use std::time::Duration; - use z3_solver::{ - ast::{Array, Ast, Bool, Dynamic, BV}, - Config, Context, SatResult, Solver as Z3Solver, Sort, - }; - - pub struct Z3SolverWrapper<'ctx> { - context: &'ctx Context, - solver: Z3Solver<'ctx>, - mapping: HashMap>, - zero: BV<'ctx>, - one: BV<'ctx>, - } - - impl<'ctx> SMTSolver for Z3SolverWrapper<'ctx> { - fn name() -> &'static str { - "Z3" - } - - fn new(timeout: Option) -> Self { - let mut config = Config::new(); - if let Some(duration) = timeout { - config.set_timeout_msec(duration.as_millis().try_into().expect("fits in u64")); - } - let context = Context::new(&config); - // TODO: This is very funky, avoid leaking context. - let leak: &'ctx Context = Box::leak(Box::new(context)); - Self { - context: leak, - solver: Z3Solver::new(leak), - mapping: HashMap::new(), - zero: BV::from_u64(leak, 0, 64), - one: BV::from_u64(leak, 1, 64), - } - } - - fn is_always_true(&mut self, node: &NodeRef) -> bool { - let z3_bool = self.visit(node).as_bool().expect("bool").not(); - self.solve_impl(&z3_bool) == SMTSolution::Unsat - } - - fn is_always_false(&mut self, node: &NodeRef) -> bool { - let z3_bool = self.visit(node).as_bool().expect("bool"); - self.solve_impl(&z3_bool) == SMTSolution::Unsat - } - - fn is_always_equal(&mut self, left: &NodeRef, right: &NodeRef) -> bool { - let z3_left = Dynamic::from_ast(self.visit(left)); - let z3_right = Dynamic::from_ast(self.visit(right)); - let z3_bool = z3_left._eq(&z3_right).not(); - self.solve_impl(&z3_bool) == SMTSolution::Unsat - } - - fn solve(&mut self, root: &NodeRef) -> SMTSolution { - let z3_bool = self.visit(root).as_bool().expect("bool"); - self.solve_impl(&z3_bool) - } - } - - impl<'ctx> Z3SolverWrapper<'ctx> { - fn solve_impl(&mut self, z3_bool: &Bool<'ctx>) -> SMTSolution { - self.solver.push(); - self.solver.assert(z3_bool); - let solution = match self.solver.check() { - SatResult::Sat => SMTSolution::Sat, - SatResult::Unsat => SMTSolution::Unsat, - SatResult::Unknown => SMTSolution::Timeout, - }; - self.solver.pop(1); - if solution == SMTSolution::Timeout { - debug!("Query timeout was reached by Z3"); - } - solution - } - - fn visit(&mut self, node: &NodeRef) -> &Dynamic<'ctx> { - let key = HashableNodeRef::from(node.clone()); - if !self.mapping.contains_key(&key) { - let value = self.translate(node); - assert!(!self.mapping.contains_key(&key)); - self.mapping.insert(key.clone(), value); - } - &self.mapping[&key] - } - - #[rustfmt::skip] - fn translate(&mut self, node: &NodeRef) -> Dynamic<'ctx> { - match &*node.borrow() { - Node::Const { sort: NodeType::Bit, imm, .. } => { - Bool::from_bool(self.context, *imm != 0).into() - } - Node::Const { sort, imm, .. } => { - let width = sort.bitsize() as u32; - BV::from_u64(self.context, *imm, width).into() - } - Node::Read { memory, address, .. } => { - let z3_memory = self.visit(memory).as_array().expect("array"); - let z3_address = self.visit(address).as_bv().expect("bv"); - z3_memory.select(&z3_address) - } - Node::Write { memory, address, value, .. } => { - let z3_memory = self.visit(memory).as_array().expect("array"); - let z3_address = self.visit(address).as_bv().expect("bv"); - let z3_value = self.visit(value).as_bv().expect("bv"); - z3_memory.store(&z3_address, &z3_value).into() - } - Node::Add { left, right, .. } => { - let z3_left = self.visit(left).as_bv().expect("bv"); - let z3_right = self.visit(right).as_bv().expect("bv"); - z3_left.bvadd(&z3_right).into() - } - Node::Sub { left, right, .. } => { - let z3_left = self.visit(left).as_bv().expect("bv"); - let z3_right = self.visit(right).as_bv().expect("bv"); - z3_left.bvsub(&z3_right).into() - } - Node::Mul { left, right, .. } => { - let z3_left = self.visit(left).as_bv().expect("bv"); - let z3_right = self.visit(right).as_bv().expect("bv"); - z3_left.bvmul(&z3_right).into() - } - Node::Divu { left, right, .. } => { - let z3_left = self.visit(left).as_bv().expect("bv"); - let z3_right = self.visit(right).as_bv().expect("bv"); - z3_left.bvudiv(&z3_right).into() - } - Node::Div { left, right, .. } => { - let z3_left = self.visit(left).as_bv().expect("bv"); - let z3_right = self.visit(right).as_bv().expect("bv"); - z3_left.bvsdiv(&z3_right).into() - } - Node::Rem { left, right, .. } => { - let z3_left = self.visit(left).as_bv().expect("bv"); - let z3_right = self.visit(right).as_bv().expect("bv"); - z3_left.bvurem(&z3_right).into() - } - Node::Sll { left, right , ..} => { - let z3_left = self.visit(left).as_bv().expect("bv"); - let z3_right = self.visit(right).as_bv().expect("bv"); - z3_left.bvshl(&z3_right).into() - }, - Node::Srl { left, right, ..} => { - let z3_left = self.visit(left).as_bv().expect("bv"); - let z3_right = self.visit(right).as_bv().expect("bv"); - z3_left.bvlshr(&z3_right).into() - }, - Node::Ult { left, right, .. } => { - let z3_left = self.visit(left).as_bv().expect("bv"); - let z3_right = self.visit(right).as_bv().expect("bv"); - z3_left.bvult(&z3_right).into() - } - Node::Ext { from: NodeType::Bit, value, .. } => { - let z3_value = self.visit(value).as_bool().expect("bool"); - z3_value.ite(&self.zero, &self.one).into() - } - Node::Ext { from, value, .. } => { - let width = from.bitsize() as u32; - let z3_value = self.visit(value).as_bv().expect("bv"); - z3_value.zero_ext(64 - width).into() - } - Node::Ite { cond, left, right, .. } => { - let z3_cond = self.visit(cond).as_bool().expect("bool"); - let z3_left = Dynamic::from_ast(self.visit(left)); - let z3_right = Dynamic::from_ast(self.visit(right)); - z3_cond.ite(&z3_left, &z3_right) - } - Node::Eq { left, right, .. } => { - let z3_left = self.visit(left).as_bv().expect("bv"); - let z3_right = self.visit(right).as_bv().expect("bv"); - z3_left._eq(&z3_right).into() - } - Node::And { sort: NodeType::Bit, left, right, .. } => { - let z3_left = self.visit(left).as_bool().expect("bool"); - let z3_right = self.visit(right).as_bool().expect("bool"); - Bool::and(self.context, &[&z3_left, &z3_right]).into() - } - Node::And { left, right, .. } => { - let z3_left = self.visit(left).as_bv().expect("bv"); - let z3_right = self.visit(right).as_bv().expect("bv"); - z3_left.bvand(&z3_right).into() - } - Node::Or { sort: NodeType::Bit, left, right, .. } => { - let z3_left = self.visit(left).as_bool().expect("bool"); - let z3_right = self.visit(right).as_bool().expect("bool"); - Bool::or(self.context, &[&z3_left, &z3_right]).into() - } - Node::Or { left, right, .. } => { - let z3_left = self.visit(left).as_bv().expect("bv"); - let z3_right = self.visit(right).as_bv().expect("bv"); - z3_left.bvor(&z3_right).into() - } - Node::Not { sort: NodeType::Bit, value, .. } => { - let z3_value = self.visit(value).as_bool().expect("bool"); - z3_value.not().into() - } - Node::Not { value, .. } => { - let z3_value = self.visit(value).as_bv().expect("bv"); - z3_value.bvnot().into() - } - Node::State { sort: NodeType::Bit, name, .. } => { - let name = name.as_deref().expect("name"); - Bool::new_const(self.context, name).into() - } - Node::State { sort: NodeType::Memory, name, .. } => { - let name = name.as_deref().expect("name"); - let bv64 = Sort::bitvector(self.context, 64); - Array::new_const(self.context, name, &bv64, &bv64).into() - } - Node::State { sort, name, .. } => { - let width = sort.bitsize() as u32; - let name = name.as_deref().expect("name"); - BV::new_const(self.context, name, width).into() - } - Node::Input { sort, name, .. } => { - let width = sort.bitsize() as u32; - BV::new_const(self.context, name.to_owned(), width).into() - } - Node::Next { .. } => panic!("should be unreachable"), - Node::Bad { cond, .. } => { - // TODO: It would be better if we would directly referece the condition instead of referencing the Bad node in the OR'ed graph. That way Bad conceptually remains as not producing any output and the graph that smt_solver.rs sees is still purely combinatorial. - self.visit(cond).clone() - }, - Node::Comment(_) => panic!("cannot translate"), - } - } - } -} diff --git a/src/unicorn/z3solver_impl.rs b/src/unicorn/z3solver_impl.rs new file mode 100644 index 00000000..cea89289 --- /dev/null +++ b/src/unicorn/z3solver_impl.rs @@ -0,0 +1,231 @@ +use crate::unicorn::smt_solver::{SMTSolution, SMTSolver}; +use crate::unicorn::{HashableNodeRef, Node, NodeRef, NodeType}; +use log::debug; +use std::collections::HashMap; +use std::convert::TryInto; +use std::time::Duration; +use z3_solver::{ + ast::{Array, Ast, Bool, Dynamic, BV}, + Config, Context, SatResult, Solver as Z3Solver, Sort, +}; + +pub struct Z3SolverWrapper<'ctx> { + context: &'ctx Context, + solver: Z3Solver<'ctx>, + mapping: HashMap>, + zero: BV<'ctx>, + one: BV<'ctx>, +} + +impl<'ctx> SMTSolver for Z3SolverWrapper<'ctx> { + fn name() -> &'static str { + "Z3" + } + + fn new(timeout: Option) -> Self { + let mut config = Config::new(); + if let Some(duration) = timeout { + config.set_timeout_msec(duration.as_millis().try_into().expect("fits in u64")); + } + let context = Context::new(&config); + // TODO: This is very funky, avoid leaking context. + let leak: &'ctx Context = Box::leak(Box::new(context)); + Self { + context: leak, + solver: Z3Solver::new(leak), + mapping: HashMap::new(), + zero: BV::from_u64(leak, 0, 64), + one: BV::from_u64(leak, 1, 64), + } + } + + fn is_always_true(&mut self, node: &NodeRef) -> bool { + let z3_bool = self.visit(node).as_bool().expect("bool").not(); + self.solve_impl(&z3_bool) == SMTSolution::Unsat + } + + fn is_always_false(&mut self, node: &NodeRef) -> bool { + let z3_bool = self.visit(node).as_bool().expect("bool"); + self.solve_impl(&z3_bool) == SMTSolution::Unsat + } + + fn is_always_equal(&mut self, left: &NodeRef, right: &NodeRef) -> bool { + let z3_left = Dynamic::from_ast(self.visit(left)); + let z3_right = Dynamic::from_ast(self.visit(right)); + let z3_bool = z3_left._eq(&z3_right).not(); + self.solve_impl(&z3_bool) == SMTSolution::Unsat + } + + fn solve(&mut self, root: &NodeRef) -> SMTSolution { + let z3_bool = self.visit(root).as_bool().expect("bool"); + self.solve_impl(&z3_bool) + } +} + +impl<'ctx> Z3SolverWrapper<'ctx> { + fn solve_impl(&mut self, z3_bool: &Bool<'ctx>) -> SMTSolution { + self.solver.push(); + self.solver.assert(z3_bool); + let solution = match self.solver.check() { + SatResult::Sat => SMTSolution::Sat, + SatResult::Unsat => SMTSolution::Unsat, + SatResult::Unknown => SMTSolution::Timeout, + }; + self.solver.pop(1); + if solution == SMTSolution::Timeout { + debug!("Query timeout was reached by Z3"); + } + solution + } + + fn visit(&mut self, node: &NodeRef) -> &Dynamic<'ctx> { + let key = HashableNodeRef::from(node.clone()); + if !self.mapping.contains_key(&key) { + let value = self.translate(node); + assert!(!self.mapping.contains_key(&key)); + self.mapping.insert(key.clone(), value); + } + &self.mapping[&key] + } + + #[rustfmt::skip] + fn translate(&mut self, node: &NodeRef) -> Dynamic<'ctx> { + match &*node.borrow() { + Node::Const { sort: NodeType::Bit, imm, .. } => { + Bool::from_bool(self.context, *imm != 0).into() + } + Node::Const { sort, imm, .. } => { + let width = sort.bitsize() as u32; + BV::from_u64(self.context, *imm, width).into() + } + Node::Read { memory, address, .. } => { + let z3_memory = self.visit(memory).as_array().expect("array"); + let z3_address = self.visit(address).as_bv().expect("bv"); + z3_memory.select(&z3_address) + } + Node::Write { memory, address, value, .. } => { + let z3_memory = self.visit(memory).as_array().expect("array"); + let z3_address = self.visit(address).as_bv().expect("bv"); + let z3_value = self.visit(value).as_bv().expect("bv"); + z3_memory.store(&z3_address, &z3_value).into() + } + Node::Add { left, right, .. } => { + let z3_left = self.visit(left).as_bv().expect("bv"); + let z3_right = self.visit(right).as_bv().expect("bv"); + z3_left.bvadd(&z3_right).into() + } + Node::Sub { left, right, .. } => { + let z3_left = self.visit(left).as_bv().expect("bv"); + let z3_right = self.visit(right).as_bv().expect("bv"); + z3_left.bvsub(&z3_right).into() + } + Node::Mul { left, right, .. } => { + let z3_left = self.visit(left).as_bv().expect("bv"); + let z3_right = self.visit(right).as_bv().expect("bv"); + z3_left.bvmul(&z3_right).into() + } + Node::Divu { left, right, .. } => { + let z3_left = self.visit(left).as_bv().expect("bv"); + let z3_right = self.visit(right).as_bv().expect("bv"); + z3_left.bvudiv(&z3_right).into() + } + Node::Div { left, right, .. } => { + let z3_left = self.visit(left).as_bv().expect("bv"); + let z3_right = self.visit(right).as_bv().expect("bv"); + z3_left.bvsdiv(&z3_right).into() + } + Node::Rem { left, right, .. } => { + let z3_left = self.visit(left).as_bv().expect("bv"); + let z3_right = self.visit(right).as_bv().expect("bv"); + z3_left.bvurem(&z3_right).into() + } + Node::Sll { left, right , ..} => { + let z3_left = self.visit(left).as_bv().expect("bv"); + let z3_right = self.visit(right).as_bv().expect("bv"); + z3_left.bvshl(&z3_right).into() + }, + Node::Srl { left, right, ..} => { + let z3_left = self.visit(left).as_bv().expect("bv"); + let z3_right = self.visit(right).as_bv().expect("bv"); + z3_left.bvlshr(&z3_right).into() + }, + Node::Ult { left, right, .. } => { + let z3_left = self.visit(left).as_bv().expect("bv"); + let z3_right = self.visit(right).as_bv().expect("bv"); + z3_left.bvult(&z3_right).into() + } + Node::Ext { from: NodeType::Bit, value, .. } => { + let z3_value = self.visit(value).as_bool().expect("bool"); + z3_value.ite(&self.zero, &self.one).into() + } + Node::Ext { from, value, .. } => { + let width = from.bitsize() as u32; + let z3_value = self.visit(value).as_bv().expect("bv"); + z3_value.zero_ext(64 - width).into() + } + Node::Ite { cond, left, right, .. } => { + let z3_cond = self.visit(cond).as_bool().expect("bool"); + let z3_left = Dynamic::from_ast(self.visit(left)); + let z3_right = Dynamic::from_ast(self.visit(right)); + z3_cond.ite(&z3_left, &z3_right) + } + Node::Eq { left, right, .. } => { + let z3_left = self.visit(left).as_bv().expect("bv"); + let z3_right = self.visit(right).as_bv().expect("bv"); + z3_left._eq(&z3_right).into() + } + Node::And { sort: NodeType::Bit, left, right, .. } => { + let z3_left = self.visit(left).as_bool().expect("bool"); + let z3_right = self.visit(right).as_bool().expect("bool"); + Bool::and(self.context, &[&z3_left, &z3_right]).into() + } + Node::And { left, right, .. } => { + let z3_left = self.visit(left).as_bv().expect("bv"); + let z3_right = self.visit(right).as_bv().expect("bv"); + z3_left.bvand(&z3_right).into() + } + Node::Or { sort: NodeType::Bit, left, right, .. } => { + let z3_left = self.visit(left).as_bool().expect("bool"); + let z3_right = self.visit(right).as_bool().expect("bool"); + Bool::or(self.context, &[&z3_left, &z3_right]).into() + } + Node::Or { left, right, .. } => { + let z3_left = self.visit(left).as_bv().expect("bv"); + let z3_right = self.visit(right).as_bv().expect("bv"); + z3_left.bvor(&z3_right).into() + } + Node::Not { sort: NodeType::Bit, value, .. } => { + let z3_value = self.visit(value).as_bool().expect("bool"); + z3_value.not().into() + } + Node::Not { value, .. } => { + let z3_value = self.visit(value).as_bv().expect("bv"); + z3_value.bvnot().into() + } + Node::State { sort: NodeType::Bit, name, .. } => { + let name = name.as_deref().expect("name"); + Bool::new_const(self.context, name).into() + } + Node::State { sort: NodeType::Memory, name, .. } => { + let name = name.as_deref().expect("name"); + let bv64 = Sort::bitvector(self.context, 64); + Array::new_const(self.context, name, &bv64, &bv64).into() + } + Node::State { sort, name, .. } => { + let width = sort.bitsize() as u32; + let name = name.as_deref().expect("name"); + BV::new_const(self.context, name, width).into() + } + Node::Input { sort, name, .. } => { + let width = sort.bitsize() as u32; + BV::new_const(self.context, name.to_owned(), width).into() + } + Node::Next { .. } => panic!("should be unreachable"), + Node::Bad { cond, .. } => { + // TODO: It would be better if we would directly referece the condition instead of referencing the Bad node in the OR'ed graph. That way Bad conceptually remains as not producing any output and the graph that smt_solver.rs sees is still purely combinatorial. + self.visit(cond).clone() + }, + Node::Comment(_) => panic!("cannot translate"), + } + } +} diff --git a/unicorn_api/.gitignore b/unicorn_api/.gitignore new file mode 100644 index 00000000..af3ca5ef --- /dev/null +++ b/unicorn_api/.gitignore @@ -0,0 +1,72 @@ +/target + +# Byte-compiled / optimized / DLL files +__pycache__/ +.pytest_cache/ +*.py[cod] + +# C extensions +*.so + +# Distribution / packaging +.Python +.venv/ +env/ +bin/ +build/ +develop-eggs/ +dist/ +eggs/ +lib/ +lib64/ +parts/ +sdist/ +var/ +include/ +man/ +venv/ +*.egg-info/ +.installed.cfg +*.egg + +# Installer logs +pip-log.txt +pip-delete-this-directory.txt +pip-selfcheck.json + +# Unit test / coverage reports +htmlcov/ +.tox/ +.coverage +.cache +nosetests.xml +coverage.xml + +# Translations +*.mo + +# Mr Developer +.mr.developer.cfg +.project +.pydevproject + +# Rope +.ropeproject + +# Django stuff: +*.log +*.pot + +.DS_Store + +# Sphinx documentation +docs/_build/ + +# PyCharm +.idea/ + +# VSCode +.vscode/ + +# Pyenv +.python-version \ No newline at end of file diff --git a/unicorn_api/Cargo.lock b/unicorn_api/Cargo.lock new file mode 100644 index 00000000..878d14c0 --- /dev/null +++ b/unicorn_api/Cargo.lock @@ -0,0 +1,811 @@ +# This file is automatically @generated by Cargo. +# It is not intended for manual editing. +version = 3 + +[[package]] +name = "aho-corasick" +version = "0.7.20" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cc936419f96fa211c1b9166887b38e5e40b19958e5b895be7c1f93adec7071ac" +dependencies = [ + "memchr", +] + +[[package]] +name = "ansi_term" +version = "0.12.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d52a9bb7ec0cf484c551830a7ce27bd20d67eac647e1befb56b0be4ee39a55d2" +dependencies = [ + "winapi", +] + +[[package]] +name = "anyhow" +version = "1.0.68" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2cb2f989d18dd141ab8ae82f64d1a8cdd37e0840f73a406896cf5e99502fab61" + +[[package]] +name = "atty" +version = "0.2.14" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d9b39be18770d11421cdb1b9947a45dd3f37e93092cbf377614828a319d5fee8" +dependencies = [ + "hermit-abi", + "libc", + "winapi", +] + +[[package]] +name = "autocfg" +version = "1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d468802bab17cbc0cc575e9b053f41e72aa36bfa6b7f55e3529ffa43161b97fa" + +[[package]] +name = "bindgen" +version = "0.58.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0f8523b410d7187a43085e7e064416ea32ded16bd0a4e6fc025e21616d01258f" +dependencies = [ + "bitflags", + "cexpr", + "clang-sys", + "clap 2.34.0", + "env_logger 0.8.4", + "lazy_static", + "lazycell", + "log", + "peeking_take_while", + "proc-macro2", + "quote", + "regex", + "rustc-hash", + "shlex", + "which", +] + +[[package]] +name = "bitflags" +version = "1.3.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a" + +[[package]] +name = "byteorder" +version = "1.4.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "14c189c53d098945499cdfa7ecc63567cf3886b3332b312a5b4585d8d3a6a610" + +[[package]] +name = "bytesize" +version = "1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6c58ec36aac5066d5ca17df51b3e70279f5670a72102f5752cb7e7c856adfc70" + +[[package]] +name = "cc" +version = "1.0.78" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a20104e2335ce8a659d6dd92a51a767a0c062599c73b343fd152cb401e828c3d" + +[[package]] +name = "cexpr" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f4aedb84272dbe89af497cf81375129abda4fc0a9e7c5d317498c15cc30c0d27" +dependencies = [ + "nom", +] + +[[package]] +name = "cfg-if" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" + +[[package]] +name = "clang-sys" +version = "1.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fa2e27ae6ab525c3d369ded447057bca5438d86dc3a68f6faafb8269ba82ebf3" +dependencies = [ + "glob", + "libc", + "libloading", +] + +[[package]] +name = "clap" +version = "2.34.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a0610544180c38b88101fecf2dd634b174a62eef6946f84dfc6a7127512b381c" +dependencies = [ + "ansi_term", + "atty", + "bitflags", + "strsim 0.8.0", + "textwrap 0.11.0", + "unicode-width", + "vec_map", +] + +[[package]] +name = "clap" +version = "3.2.23" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "71655c45cb9845d3270c9d6df84ebe72b4dad3c2ba3f7023ad47c144e4e473a5" +dependencies = [ + "atty", + "bitflags", + "clap_lex", + "indexmap", + "once_cell", + "strsim 0.10.0", + "termcolor", + "textwrap 0.16.0", +] + +[[package]] +name = "clap_lex" +version = "0.2.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2850f2f5a82cbf437dd5af4d49848fbdfc27c157c3d010345776f952765261c5" +dependencies = [ + "os_str_bytes", +] + +[[package]] +name = "cmake" +version = "0.1.49" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "db34956e100b30725f2eb215f90d4871051239535632f84fea3bc92722c66b7c" +dependencies = [ + "cc", +] + +[[package]] +name = "env_logger" +version = "0.8.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a19187fea3ac7e84da7dacf48de0c45d63c6a76f9490dae389aead16c243fce3" +dependencies = [ + "atty", + "humantime", + "log", + "regex", + "termcolor", +] + +[[package]] +name = "env_logger" +version = "0.9.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a12e6657c4c97ebab115a42dcee77225f7f482cdd841cf7088c657a42e9e00e7" +dependencies = [ + "atty", + "humantime", + "log", + "regex", + "termcolor", +] + +[[package]] +name = "glob" +version = "0.3.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d2fabcfbdc87f4758337ca535fb41a6d701b65693ce38287d856d1674551ec9b" + +[[package]] +name = "goblin" +version = "0.3.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "669cdc3826f69a51d3f8fc3f86de81c2378110254f678b8407977736122057a4" +dependencies = [ + "log", + "plain", + "scroll", +] + +[[package]] +name = "hashbrown" +version = "0.12.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8a9ee70c43aaf417c914396645a0fa852624801b24ebb7ae78fe8272889ac888" + +[[package]] +name = "heck" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2540771e65fc8cb83cd6e8a237f70c319bd5c29f78ed1084ba5d50eeac86f7f9" + +[[package]] +name = "hermit-abi" +version = "0.1.19" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "62b467343b94ba476dcb2500d242dadbb39557df889310ac77c5d99100aaac33" +dependencies = [ + "libc", +] + +[[package]] +name = "humantime" +version = "2.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9a3a5bfb195931eeb336b2a7b4d761daec841b97f947d34394601737a7bba5e4" + +[[package]] +name = "indexmap" +version = "1.9.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1885e79c1fc4b10f0e172c475f458b7f7b93061064d98c3293e98c5ba0c8b399" +dependencies = [ + "autocfg", + "hashbrown", +] + +[[package]] +name = "indoc" +version = "1.0.8" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "da2d6f23ffea9d7e76c53eee25dfb67bcd8fde7f1198b0855350698c9f07c780" + +[[package]] +name = "lazy_static" +version = "1.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e2abad23fbc42b3700f2f279844dc832adb2b2eb069b2df918f455c4e18cc646" + +[[package]] +name = "lazycell" +version = "1.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "830d08ce1d1d941e6b30645f1a0eb5643013d835ce3779a5fc208261dbe10f55" + +[[package]] +name = "libc" +version = "0.2.139" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "201de327520df007757c1f0adce6e827fe8562fbc28bfd9c15571c66ca1f5f79" + +[[package]] +name = "libloading" +version = "0.7.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b67380fd3b2fbe7527a606e18729d21c6f3951633d0500574c4dc22d2d638b9f" +dependencies = [ + "cfg-if", + "winapi", +] + +[[package]] +name = "lock_api" +version = "0.4.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "435011366fe56583b16cf956f9df0095b405b82d76425bc8981c0e22e60ec4df" +dependencies = [ + "autocfg", + "scopeguard", +] + +[[package]] +name = "log" +version = "0.4.17" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "abb12e687cfb44aa40f41fc3978ef76448f9b6038cad6aef4259d3c095a2382e" +dependencies = [ + "cfg-if", +] + +[[package]] +name = "memchr" +version = "2.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2dffe52ecf27772e601905b7522cb4ef790d2cc203488bbd0e2fe85fcb74566d" + +[[package]] +name = "memoffset" +version = "0.6.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5aa361d4faea93603064a027415f07bd8e1d5c88c9fbf68bf56a285428fd79ce" +dependencies = [ + "autocfg", +] + +[[package]] +name = "nom" +version = "5.1.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ffb4262d26ed83a1c0a33a38fe2bb15797329c85770da05e6b828ddb782627af" +dependencies = [ + "memchr", + "version_check", +] + +[[package]] +name = "once_cell" +version = "1.17.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6f61fba1741ea2b3d6a1e3178721804bb716a68a6aeba1149b5d52e3d464ea66" + +[[package]] +name = "os_str_bytes" +version = "6.4.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9b7820b9daea5457c9f21c69448905d723fbd21136ccf521748f23fd49e723ee" + +[[package]] +name = "parking_lot" +version = "0.12.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3742b2c103b9f06bc9fff0a37ff4912935851bee6d36f3c02bcc755bcfec228f" +dependencies = [ + "lock_api", + "parking_lot_core", +] + +[[package]] +name = "parking_lot_core" +version = "0.9.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ba1ef8814b5c993410bb3adfad7a5ed269563e4a2f90c41f5d85be7fb47133bf" +dependencies = [ + "cfg-if", + "libc", + "redox_syscall", + "smallvec", + "windows-sys", +] + +[[package]] +name = "peeking_take_while" +version = "0.1.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "19b17cddbe7ec3f8bc800887bab5e717348c95ea2ca0b1bf0837fb964dc67099" + +[[package]] +name = "plain" +version = "0.2.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b4596b6d070b27117e987119b4dac604f3c58cfb0b191112e24771b2faeac1a6" + +[[package]] +name = "proc-macro2" +version = "1.0.50" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6ef7d57beacfaf2d8aee5937dab7b7f28de3cb8b1828479bb5de2a7106f2bae2" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "pyo3" +version = "0.17.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "268be0c73583c183f2b14052337465768c07726936a260f480f0857cb95ba543" +dependencies = [ + "cfg-if", + "indoc", + "libc", + "memoffset", + "parking_lot", + "pyo3-build-config", + "pyo3-ffi", + "pyo3-macros", + "unindent", +] + +[[package]] +name = "pyo3-build-config" +version = "0.17.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "28fcd1e73f06ec85bf3280c48c67e731d8290ad3d730f8be9dc07946923005c8" +dependencies = [ + "once_cell", + "target-lexicon", +] + +[[package]] +name = "pyo3-ffi" +version = "0.17.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0f6cb136e222e49115b3c51c32792886defbfb0adead26a688142b346a0b9ffc" +dependencies = [ + "libc", + "pyo3-build-config", +] + +[[package]] +name = "pyo3-macros" +version = "0.17.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "94144a1266e236b1c932682136dc35a9dee8d3589728f68130c7c3861ef96b28" +dependencies = [ + "proc-macro2", + "pyo3-macros-backend", + "quote", + "syn", +] + +[[package]] +name = "pyo3-macros-backend" +version = "0.17.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c8df9be978a2d2f0cdebabb03206ed73b11314701a5bfe71b0d753b81997777f" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "quote" +version = "1.0.23" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8856d8364d252a14d474036ea1358d63c9e6965c8e5c1885c18f73d70bff9c7b" +dependencies = [ + "proc-macro2", +] + +[[package]] +name = "redox_syscall" +version = "0.2.16" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fb5a58c1855b4b6819d59012155603f0b22ad30cad752600aadfcb695265519a" +dependencies = [ + "bitflags", +] + +[[package]] +name = "regex" +version = "1.6.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4c4eb3267174b8c6c2f654116623910a0fef09c4753f8dd83db29c48a0df988b" +dependencies = [ + "aho-corasick", + "memchr", + "regex-syntax", +] + +[[package]] +name = "regex-syntax" +version = "0.6.28" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "456c603be3e8d448b072f410900c09faf164fbce2d480456f50eea6e25f9c848" + +[[package]] +name = "riscu" +version = "0.5.0" +source = "git+https://github.com/cksystemsgroup/riscu#de3cfede9c770336b1b2fe356e68f270dc375237" +dependencies = [ + "byteorder", + "goblin", + "log", + "thiserror", +] + +[[package]] +name = "rustc-hash" +version = "1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "08d43f7aa6b08d49f382cde6a7982047c3426db949b1424bc4b7ec9ae12c6ce2" + +[[package]] +name = "rustversion" +version = "1.0.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5583e89e108996506031660fe09baa5011b9dd0341b89029313006d1fb508d70" + +[[package]] +name = "scopeguard" +version = "1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d29ab0c6d3fc0ee92fe66e2d99f700eab17a8d57d1c1d3b748380fb20baa78cd" + +[[package]] +name = "scroll" +version = "0.10.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fda28d4b4830b807a8b43f7b0e6b5df875311b3e7621d84577188c175b6ec1ec" +dependencies = [ + "scroll_derive", +] + +[[package]] +name = "scroll_derive" +version = "0.10.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "aaaae8f38bb311444cfb7f1979af0bc9240d95795f75f9ceddf6a59b79ceffa0" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "shlex" +version = "1.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "43b2853a4d09f215c24cc5489c992ce46052d359b5109343cbafbf26bc62f8a3" + +[[package]] +name = "smallvec" +version = "1.10.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a507befe795404456341dfab10cef66ead4c041f62b8b11bbb92bffe5d0953e0" + +[[package]] +name = "strsim" +version = "0.8.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8ea5119cdb4c55b55d432abb513a0429384878c15dde60cc77b1c99de1a95a6a" + +[[package]] +name = "strsim" +version = "0.10.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "73473c0e59e6d5812c5dfe2a064a6444949f089e20eec9a2e5506596494e4623" + +[[package]] +name = "strum" +version = "0.24.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "063e6045c0e62079840579a7e47a355ae92f60eb74daaf156fb1e84ba164e63f" +dependencies = [ + "strum_macros", +] + +[[package]] +name = "strum_macros" +version = "0.24.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1e385be0d24f186b4ce2f9982191e7101bb737312ad61c1f2f984f34bcf85d59" +dependencies = [ + "heck", + "proc-macro2", + "quote", + "rustversion", + "syn", +] + +[[package]] +name = "syn" +version = "1.0.107" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1f4064b5b16e03ae50984a5a8ed5d4f8803e6bc1fd170a3cda91a1be4b18e3f5" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "target-lexicon" +version = "0.12.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9410d0f6853b1d94f0e519fb95df60f29d2c1eff2d921ffdf01a4c8a3b54f12d" + +[[package]] +name = "termcolor" +version = "1.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "be55cf8942feac5c765c2c993422806843c9a9a45d4d5c407ad6dd2ea95eb9b6" +dependencies = [ + "winapi-util", +] + +[[package]] +name = "textwrap" +version = "0.11.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d326610f408c7a4eb6f51c37c330e496b08506c9457c9d34287ecc38809fb060" +dependencies = [ + "unicode-width", +] + +[[package]] +name = "textwrap" +version = "0.16.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "222a222a5bfe1bba4a77b45ec488a741b3cb8872e5e499451fd7d0129c9c7c3d" + +[[package]] +name = "thiserror" +version = "1.0.38" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6a9cd18aa97d5c45c6603caea1da6628790b37f7a34b6ca89522331c5180fed0" +dependencies = [ + "thiserror-impl", +] + +[[package]] +name = "thiserror-impl" +version = "1.0.38" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1fb327af4685e4d03fa8cbcf1716380da910eeb2bb8be417e7f9fd3fb164f36f" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "unicode-ident" +version = "1.0.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "84a22b9f218b40614adcb3f4ff08b703773ad44fa9423e4e0d346d5db86e4ebc" + +[[package]] +name = "unicode-width" +version = "0.1.10" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c0edd1e5b14653f783770bce4a4dabb4a5108a5370a5f5d8cfe8710c361f6c8b" + +[[package]] +name = "unicorn-rs" +version = "0.4.1" +source = "git+https://github.com/cksystemsgroup/unicorn?branch=opt-quarc-paper#5a6a8228a14a33a870719241caddb8432f2d0787" +dependencies = [ + "anyhow", + "byteorder", + "bytesize", + "clap 3.2.23", + "env_logger 0.9.3", + "log", + "pyo3", + "regex", + "riscu", + "strum", + "thiserror", + "z3", + "z3-sys", +] + +[[package]] +name = "unicorn_api" +version = "0.1.0" +dependencies = [ + "bytesize", + "pyo3", + "riscu", + "unicorn-rs", + "z3", + "z3-sys", +] + +[[package]] +name = "unindent" +version = "0.1.11" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e1766d682d402817b5ac4490b3c3002d91dfa0d22812f341609f97b08757359c" + +[[package]] +name = "vec_map" +version = "0.8.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f1bddf1187be692e79c5ffeab891132dfb0f236ed36a43c7ed39f1165ee20191" + +[[package]] +name = "version_check" +version = "0.9.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "49874b5167b65d7193b8aba1567f5c7d93d001cafc34600cee003eda787e483f" + +[[package]] +name = "which" +version = "3.1.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d011071ae14a2f6671d0b74080ae0cd8ebf3a6f8c9589a2cd45f23126fe29724" +dependencies = [ + "libc", +] + +[[package]] +name = "winapi" +version = "0.3.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5c839a674fcd7a98952e593242ea400abe93992746761e38641405d28b00f419" +dependencies = [ + "winapi-i686-pc-windows-gnu", + "winapi-x86_64-pc-windows-gnu", +] + +[[package]] +name = "winapi-i686-pc-windows-gnu" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6" + +[[package]] +name = "winapi-util" +version = "0.1.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "70ec6ce85bb158151cae5e5c87f95a8e97d2c0c4b001223f33a334e3ce5de178" +dependencies = [ + "winapi", +] + +[[package]] +name = "winapi-x86_64-pc-windows-gnu" +version = "0.4.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" + +[[package]] +name = "windows-sys" +version = "0.42.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5a3e1820f08b8513f676f7ab6c1f99ff312fb97b553d30ff4dd86f9f15728aa7" +dependencies = [ + "windows_aarch64_gnullvm", + "windows_aarch64_msvc", + "windows_i686_gnu", + "windows_i686_msvc", + "windows_x86_64_gnu", + "windows_x86_64_gnullvm", + "windows_x86_64_msvc", +] + +[[package]] +name = "windows_aarch64_gnullvm" +version = "0.42.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8c9864e83243fdec7fc9c5444389dcbbfd258f745e7853198f365e3c4968a608" + +[[package]] +name = "windows_aarch64_msvc" +version = "0.42.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4c8b1b673ffc16c47a9ff48570a9d85e25d265735c503681332589af6253c6c7" + +[[package]] +name = "windows_i686_gnu" +version = "0.42.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "de3887528ad530ba7bdbb1faa8275ec7a1155a45ffa57c37993960277145d640" + +[[package]] +name = "windows_i686_msvc" +version = "0.42.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bf4d1122317eddd6ff351aa852118a2418ad4214e6613a50e0191f7004372605" + +[[package]] +name = "windows_x86_64_gnu" +version = "0.42.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c1040f221285e17ebccbc2591ffdc2d44ee1f9186324dd3e84e99ac68d699c45" + +[[package]] +name = "windows_x86_64_gnullvm" +version = "0.42.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "628bfdf232daa22b0d64fdb62b09fcc36bb01f05a3939e20ab73aaf9470d0463" + +[[package]] +name = "windows_x86_64_msvc" +version = "0.42.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "447660ad36a13288b1db4d4248e857b510e8c3a225c822ba4fb748c0aafecffd" + +[[package]] +name = "z3" +version = "0.11.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d25754b4bf4516a65d0e596ea9c1f0082224bdf20823a37fdd9111fa08d5bf48" +dependencies = [ + "lazy_static", + "log", + "z3-sys", +] + +[[package]] +name = "z3-sys" +version = "0.7.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1c82dcbc58be4bf1994c520066cb2bd6c3d36aed0fdc57244f34d277421986a6" +dependencies = [ + "bindgen", + "cmake", +] diff --git a/unicorn_api/Cargo.toml b/unicorn_api/Cargo.toml new file mode 100644 index 00000000..68d5e165 --- /dev/null +++ b/unicorn_api/Cargo.toml @@ -0,0 +1,22 @@ +[package] +name = "unicorn_api" +version = "0.1.0" +edition = "2021" + +# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html +[lib] +name = "unicorn_api" +crate-type = ["cdylib"] + +[dependencies] +riscu = "~0.5" +pyo3 = { version = "0.17.3", features = ["auto-initialize"] } +bytesize = "~1.1" +unicorn-rs = { git = 'https://github.com/cksystemsgroup/unicorn', branch = 'opt-quarc-paper', features = ["z3"] } +z3-solver = { package = "z3", version = "~0.11", features = ["static-link-z3"]} +z3-sys = { version = "~0", features = ["static-link-z3"] } + +[patch.crates-io] +# TODO: Allows us to work on `riscu` and `unicorn` in parallel. Remove +# once `riscu` stabilizes and we made another crates.io release of it. +riscu = { git = 'https://github.com/cksystemsgroup/riscu' } diff --git a/unicorn_api/README.md b/unicorn_api/README.md new file mode 100644 index 00000000..5f8987ed --- /dev/null +++ b/unicorn_api/README.md @@ -0,0 +1,58 @@ +# Unicorn API +You will need to install [maturin](https://www.maturin.rs/installation.htm) and create a virtual environment in Python. Finally, just type `maturin develop` to install the unicorn API in your virtual environment. + +You can algo generate additional documentation using `cargo doc`. This will create a `docs` folder in `unicorn_api/target/`. + +Also, there is an example of how to build Grover algorithm with pyqir using quarc's output in `unicorn_api/examples`. Just `cd unicorn_api/examples` and invoke `python3 example_qir.py`. + +## QUARC + +Note: This tutorials assume you are in `unicorn_api/` directory. Additionally, our integer representation at bit level is LSB. + +### Some Objects + +```rust +// all these objects are dictionaries when used in Python + +struct PyQubit { + // each qubit has a unique id. Also, division and remainder create dependecies. Qubits that have a dependency should be initialized to |+>. + id: u64, + dependency: Option +} + +struct PyQuantumGate { + // Quantum gates are represented in terms of controls and target. For X gates only the target is set. + controls: Vec, + target: PyQubit +} + +struct PyDependency { + id: u64, // each dependency has a unique id + name: String, // is either "div" or "rem" + operands: Vec>, // there should be only two operands +} + +``` +### Building a quantum circuit from a binary + +We can build an optimized quantum oracle by doing: + +```Python +from unicorn_api import get_qc_from_binary + +# it uses z3 to optimize the circuit +quantum_circuit = get_qc_from_binary("../examples/selfie/d.m", # path to the binary + 86, # number of state transitions + 8, # Max number of words that the HEAP can use + 32, # Max number of words that the STACK can use + 1) # Memory size in MiB +oracle_output = quantum_circuit["oracle_output"] # id of the qubit that represents the oracle output + +circuit_stack = quantum_circuit["circuit_stack"] # This is a vector of PyQuantumGates. When uncomputing, you may want to uncompute all gates but the last one since this is the one that affects the oracle's output. + +input_qubits = quantum_circuit["input_qubits"] # this is a vector of integers, that contain the ids of the qubits that represent the input of the program and the ones we want to search for. + +dependencies = quantum_circuit["dependencies"] # Division and remainder are stated as constraints and this is a dictionary that maps PyDependency -> Vec. By solving, this specific PyDependency the value of Vec can be determined. +``` + + diff --git a/unicorn_api/examples/example_qir.py b/unicorn_api/examples/example_qir.py new file mode 100644 index 00000000..fb9865b5 --- /dev/null +++ b/unicorn_api/examples/example_qir.py @@ -0,0 +1,105 @@ +from typing import Dict, List +from unicorn_api import get_qc_from_binary +import pyqir +from utils_qir import * +from math import ceil + +def get_pyqir_grover(path: str, unroll: int, max_heap: int = 8, max_stack: int = 32, memory_size: int = 1) : + ''' + It created a QIR module of grover algorithm to search for bad-states in the file specified by path + This function returns: + 1. A module that is the oracle + 2. A List of IDs of qubits which are the input we must search using Grover Algorithm + ''' + + quantum_circuit_data = get_qc_from_binary(path, unroll, max_heap, max_stack, memory_size) + circuit_stack = quantum_circuit_data["circuit_stack"] + input_qubits = quantum_circuit_data["input_qubits"] + dependencies = quantum_circuit_data["dependencies"] + + # since PyQIR does not yet implements arbitrary MCX gates we will implement it from scratch using ancilla_max_count ancillas at most. + max_controls_in_circuit = get_max_controls_in_gates(circuit_stack) + ancillas_mcx_count = max_controls_in_circuit - 2 + + # get a dictionary (mapping_ids) that maps QIR module qubit indices to the ids the unicorn outputs. Instead, ancilla_qir_indices, are the indices used in QIR module for ancillas in MCX gates + mapping_ids, ancilla_qir_indices = init_vars(quantum_circuit_data, ancillas_mcx_count) + oracle_id = mapping_ids[quantum_circuit_data["oracle_output"]["id"]] + + # some checks + count_input = len(input_qubits) + len(dependencies) + last_gate = circuit_stack[len(circuit_stack)-1] + last_gate_controls_ids = get_vec_local_ids(mapping_ids, last_gate["controls"]) + print("last gate controls ", len(last_gate_controls_ids)) + for c in last_gate_controls_ids: + assert(oracle_id != c) + last_gate_target = mapping_ids[last_gate["target"]["id"]] + print(last_gate_target, oracle_id) + assert(last_gate_target == oracle_id) + # ------------------------------------------ + + # init QIR module + module = pyqir.SimpleModule(f"grover({path})", num_qubits=len(mapping_ids.keys()) + ancillas_mcx_count, num_results=len(input_qubits)) + qis = pyqir.BasicQisBuilder(module.builder) + + void = pyqir.Type.void(module.context) + ccx_function = module.add_external_function("ccx", pyqir.FunctionType(void, [pyqir.qubit_type(module.context), pyqir.qubit_type(module.context), pyqir.qubit_type(module.context)])) + + + # GROVER algorithm starts here + + # initialize input qubits to |+> + all_inputs = [] + for qubit in get_vec_local_ids(mapping_ids, input_qubits): + all_inputs.append(qubit) + qis.h(module.qubits[qubit]) + for target_qubits in dependencies.values(): + for qubit in get_vec_local_ids(target_qubits): + all_inputs.append(qubit) + qis.h(module.qubits[qubit]) + + # initialize oracle_output to |-> + qis.x(module.qubits[oracle_id]) + qis.h(module.qubits[oracle_id]) + + for _ in range(ceil(2**(count_input/2))): + + # apply oracle + for gate in circuit_stack: + controls = get_vec_local_ids(mapping_ids, gate["controls"]) + qir_apply_gate(qis, module, controls, mapping_ids[gate["target"]["id"]], ancilla_qir_indices, ccx_function) + + # uncompute oracle, without uncomputing the oracle's output + for gate in circuit_stack[len(circuit_stack)-2::-1]: + controls = get_vec_local_ids(mapping_ids, gate["controls"]) + for c in controls: + assert(c != oracle_id) + target = mapping_ids[gate["target"]["id"]] + qir_apply_gate(qis, module, controls, target, ancilla_qir_indices, ccx_function) + + # apply inversion above average procedure + for qubit in all_inputs: + qis.h(module.qubits[qubit]) + qis.x(module.qubits[qubit]) + + # multi-controlled Z + qis.h(module.qubits[all_inputs[0]]) + apply_mcx_gate(qis, module, all_inputs[1:], all_inputs[0], ancilla_qir_indices, ccx_function) + qis.h(module.qubits[all_inputs[0]]) + + # apply inversion above average procedure + for qubit in all_inputs: + qis.h(module.qubits[qubit]) + qis.x(module.qubits[qubit]) + + # measure result + for (index, qubit) in enumerate(input_qubits): + qis.mz(module.qubits[mapping_ids[qubit["id"]]], module.results[index]) + + return module.ir() + +print("file: d.m") +qir_ir = get_pyqir_grover("../../examples/selfie/d.m", 84) +file = open("d.qir", "w") +file.write(qir_ir) +file.close() + diff --git a/unicorn_api/examples/utils_qir.py b/unicorn_api/examples/utils_qir.py new file mode 100644 index 00000000..a9e67807 --- /dev/null +++ b/unicorn_api/examples/utils_qir.py @@ -0,0 +1,98 @@ +from typing import Dict, List, Tuple, Any +from pyqir import BasicQisBuilder, SimpleModule + +def get_vec_local_ids(mapping_ids: Dict[int, int], qubits: List[Dict]) -> List[int]: + ''' + returns a vector of QIR indices used in the a module, where mapping ids maps QUARC qubit's ids to QIR indices. + ''' + ans = [] + for qubit in qubits: + ans.append(mapping_ids[qubit["id"]]) + return ans + +def insert_new_id(mapping_ids: Dict[int, int], local_id: int, id: int) -> Tuple[bool, int]: + '''' + mapping_ids map a QUARC qubit's id to a indices in a QIR module. This function updates mapping_ids to contain local_id (QIR index). + ''' + if id in mapping_ids.keys(): + return False, local_id + else: + mapping_ids[id] = local_id + return True, local_id + 1 + +def init_vars(quantum_circuit_data: Dict[str, Any], ancillas_mcx_count: int) -> Tuple[Dict[int, int], List[int]]: + ''' + returns: + - mapping_ids: maps QUARC qubit's ids to the indices used in QIR module + - ancillas_ids: a list of QIR indices used for MCX gates + ''' + local_id = 2 + mapping_ids = dict({0: 0, 1: 1}) + + input_qubits = quantum_circuit_data["input_qubits"] + for qubit in input_qubits: + _, local_id = insert_new_id(mapping_ids, local_id, qubit['id']) + + ancillas_ids = [] + for _ in range(ancillas_mcx_count): + ancillas_ids.append(local_id) + local_id += 1 + + oracle_output = quantum_circuit_data["oracle_output"]["id"] + _, local_id = insert_new_id(mapping_ids, local_id, oracle_output) + circuit_stack = quantum_circuit_data["circuit_stack"] + for gate in circuit_stack: + for c in gate["controls"]: + _, local_id = insert_new_id(mapping_ids, local_id, c["id"]) + _, local_id, insert_new_id(mapping_ids, local_id, gate["target"]["id"]) + return mapping_ids, ancillas_ids + +def get_max_controls_in_gates(circuit_stack) -> int: + ''' + given a circuit stack it returns the maximum number of controls in all gates. + ''' + answer = 0 + for gate in circuit_stack: + answer = max(answer, len(gate["controls"])) + return answer + +def apply_mcx_gate(qis: BasicQisBuilder, module: SimpleModule, controls: List[int], target: int, ancilla_indices: List[int], ccx_function: Any): + ''' + tries to apply an MCX gate with arbitrary controls. + ''' + if len(controls) == 0: + raise Exception("MCX gates cannot be applied with 0 controls") + elif len(controls) == 1: + qis.cx(module.qubits[controls[0]], module.qubits[target]) + elif len(controls) == 2: + module.builder.call(ccx_function, [module.qubits[controls[0]], module.qubits[controls[1]], module.qubits[target]]) + else: + # this is a custom MCX gate + current_ancilla = 0 + module.builder.call(ccx_function, [module.qubits[controls[0]], module.qubits[controls[1]], module.qubits[ancilla_indices[current_ancilla]]]) + current_ancilla += 1 + + to_reverse = [] + for i in range(2, len(controls)-1): + module.builder.call(ccx_function, [module.qubits[controls[i]], + module.qubits[ancilla_indices[current_ancilla-1]], + module.qubits[ancilla_indices[current_ancilla]]]) + to_reverse.append([controls[i], ancilla_indices[current_ancilla-1], ancilla_indices[current_ancilla]]) + current_ancilla += 1 + + + module.builder.call(ccx_function, [module.qubits[controls[i]], + module.qubits[ancilla_indices[current_ancilla-1]], + module.qubits[target]]) + + # free up ancillas + for gate in to_reverse[::-1]: + module.builder.call(ccx_function, [module.qubits[gate[0]],module.qubits[gate[1]], module.qubits[gate[2]]]) + + + +def qir_apply_gate(qis: BasicQisBuilder, module: SimpleModule, controls: List[int], target: int, ancilla_indices: List[int], ccx_function: Any) : + if len(controls) == 0: + qis.x(module.qubits[target]) + elif len(controls) == 1: + apply_mcx_gate(qis, module, controls, target, ancilla_indices, ccx_function) diff --git a/unicorn_api/pyproject.toml b/unicorn_api/pyproject.toml new file mode 100644 index 00000000..48c5c0fb --- /dev/null +++ b/unicorn_api/pyproject.toml @@ -0,0 +1,14 @@ +[build-system] +requires = ["maturin>=0.14,<0.15"] +build-backend = "maturin" + +[project] +name = "unicorn_api" +requires-python = ">=3.7" +classifiers = [ + "Programming Language :: Rust", + "Programming Language :: Python :: Implementation :: CPython", + "Programming Language :: Python :: Implementation :: PyPy", +] + + diff --git a/unicorn_api/src/lib.rs b/unicorn_api/src/lib.rs new file mode 100644 index 00000000..55a8e39e --- /dev/null +++ b/unicorn_api/src/lib.rs @@ -0,0 +1,254 @@ +use std::{path::PathBuf, cell::RefCell}; + +use pyo3::{prelude::*, types::PyDict}; +use riscu::load_object_file; +use unicorn::{unicorn::{quarc::{QuantumCircuit, Unitary, QubitRef, get_constant, get_qubit_dependecy, get_dependency_data}, builder::generate_model, btor2file_parser::parse_btor2_file, memory::replace_memory, unroller::{unroll_model, prune_model, renumber_model}, optimize::optimize_model}}; +use bytesize::ByteSize; +use unicorn::unicorn::z3solver_impl; +use std::collections::HashMap; +use unicorn::unicorn::quarc::HashableDependencyRef; + +struct PyDependency { + // each dependency has a unique id + id: u64, + // is either "div" or "rem" + name: String, + // there should be only two operands + operands: Vec>, +} + +#[doc(hidden)] +impl PyDependency { + pub fn new(id: u64, name: &String, operands: &Vec>) -> Self { + Self{ + id, + name: name.to_string(), + operands: operands.to_vec() + } + } +} + +#[doc(hidden)] +impl ToPyObject for PyDependency { + // return a valid Python object + fn to_object(&self, py: Python<'_>) -> PyObject { + + let dict = PyDict::new(py); + let _ = dict.set_item("id", self.id.to_object(py)); + let _ =dict.set_item("name", self.name.to_object(py)); + let mut operands : Vec> = Vec::new(); + for operand in self.operands.iter() { + operands.push(get_pyqubit_vec(operand)); + } + + let _ = dict.set_item("target", operands.to_object(py)); + dict.to_object(py) + } +} + + +struct PyQubit { + // In Python interface you can access each of this elements as if a dictionary: qubit["id"] or qubit["dependency"]. + // each qubit has a unique id. Also, division and remainder create dependecies. Qubits that have a dependency should be initialized to |+>. + id: u64, + dependency: Option +} + +#[doc(hidden)] +impl PyQubit { + pub fn new(qubit: &QubitRef) -> Self { + let id; + if let Some(val) = get_constant(qubit) { + if val { + id = 1; + } else { + id = 0; + } + } else { + id = RefCell::as_ptr(qubit) as u64; + } + + let dep_ = get_qubit_dependecy(qubit); + let pydep = if let Some(dep) = dep_ { + Some(PyDependency::new(dep.0, &dep.1, &dep.2)) + } else { + None + }; + + Self{ + id: id, + dependency: pydep + } + } +} + +#[doc(hidden)] +impl ToPyObject for PyQubit { + // return a valid Python object + fn to_object(&self, py: Python<'_>) -> PyObject { + let dict = PyDict::new(py); + let _ =dict.set_item("id", self.id.to_object(py)); + let _ = dict.set_item("dependency", self.dependency.to_object(py)); + dict.to_object(py) + } +} + + +struct PyQuantumGate { + // Quantum gates are represented in terms of controls and target, for X gates only the target is set. + controls: Vec, + target: PyQubit +} + +#[doc(hidden)] +impl ToPyObject for PyQuantumGate { + fn to_object(&self, py: Python<'_>) -> PyObject { + let dict = PyDict::new(py); + let _ =dict.set_item("controls", self.controls.to_object(py)); + let _ = dict.set_item("target", self.target.to_object(py)); + dict.to_object(py) + } +} + +#[doc(hidden)] +fn get_pyqubit_vec(qubits: &[QubitRef]) -> Vec { + // given a vector of qubits in rust, we return a vector of qubits for Python + let mut answer = vec![]; + for qubit in qubits.iter() { + answer.push(PyQubit::new(qubit)); + } + answer +} + +#[doc(hidden)] +impl PyQuantumGate { + pub fn new(controls_: &[QubitRef], target_: &QubitRef) -> Self { + Self{ + controls: get_pyqubit_vec(controls_), + target: PyQubit::new(target_) + } + } +} + + +struct PyQuantumCircuit { + circuit_stack: Vec, + input_qubits: Vec, + dependencies: HashMap>, + oracle_output: PyQubit +} + +#[doc(hidden)] +impl PyQuantumCircuit { + pub fn new(circuit_stack: Vec, input_qubits: &[QubitRef], oracle_output: &QubitRef, dependencies: HashMap>) -> Self { + Self{ + // a vector of PyQuantumGates (only NOTs and CNOTs) + circuit_stack, + // ids of the qubits that are the inputs of the quantum circuit + input_qubits: get_pyqubit_vec(input_qubits), + // the id of the qubit that represents the outputs of oracle + oracle_output: PyQubit::new(oracle_output), + // maps a Dependency -> what set of qubits it solves in LSB + dependencies + } + } +} + +impl ToPyObject for PyQuantumCircuit { + fn to_object(&self, py: Python<'_>) -> PyObject { + + let dependencies = PyDict::new(py); + for (key, value) in self.dependencies.iter() { + let target = get_pyqubit_vec(value); + let (id, name, operands) = get_dependency_data(key); + let _ = dependencies.set_item(PyDependency::new(id, &name, &operands), target); + + } + + let dict = PyDict::new(py); + let _ =dict.set_item("circuit_stack", self.circuit_stack.to_object(py)); + let _ = dict.set_item("input_qubits", self.input_qubits.to_object(py)); + let _ = dict.set_item("oracle_output", self.oracle_output.to_object(py)); + let _ = dict.set_item("dependencies", dependencies); + dict.to_object(py) + } +} + +#[pyfunction] +fn get_qc_from_binary(path: String, unroll: usize, max_heap: u32, max_stack: u32, memory_size_: u64) -> Py { + // returns PyQuantumCircuit + let input = PathBuf::from(path.clone()); + let memory_size = ByteSize::mib(memory_size_).as_u64(); + let prune = true; + let extras = ["--fast-minimize".to_string(), "-p".to_string()].to_vec(); + + let model = { + let mut model = if true { + let program = load_object_file(&input).expect("could not load object file"); + let argv = [vec![path], extras].concat(); + generate_model(&program, memory_size, max_heap, max_stack, &argv).expect("error generating model") + } else { + parse_btor2_file(&input) + }; + + + model.lines.clear(); + replace_memory(&mut model); + for n in 0..unroll { + unroll_model(&mut model, n); + } + if prune { + prune_model(&mut model); + } + + optimize_model::(&mut model); + renumber_model(&mut model); + Some(model) + }; + + + let m = model.unwrap(); + let mut qc = QuantumCircuit::new(&m, 64); // 64 is a paramater describing wordsize + let _ = qc.process_model(1); + + let mut py_circuit_stack: Vec = vec![]; + + + for gate in qc.circuit_stack.iter() { + match &*gate.as_ref().borrow() { + Unitary::Not { input } => { + py_circuit_stack.push(PyQuantumGate::new(&vec![], input)); + }, + Unitary::Cnot { control, target } => { + py_circuit_stack.push(PyQuantumGate::new(&vec![control.clone()], target)); + }, + Unitary::Mcx { + controls, + target, + } => { + py_circuit_stack.push(PyQuantumGate::new(controls, target)); + }, + Unitary::Barrier => {} + } + + } + + let mut input_qubits = vec![]; + + for (_, qubit) in qc.input_qubits.iter() { + input_qubits.extend(qubit.clone()); + } + + + + Python::with_gil(|py| { + PyQuantumCircuit::new(py_circuit_stack, &input_qubits, &qc.output_oracle.unwrap(), qc.dependencies).to_object(py) + }) +} + +// A Python module implemented in Rust. +#[pymodule] +fn unicorn_api(_py: Python, m: &PyModule) -> PyResult<()> { + m.add_function(wrap_pyfunction!(get_qc_from_binary, m)?)?; + Ok(()) +} \ No newline at end of file