QUARC

README.md

@@ -57,17 +57,59 @@ selfie -c <SOURCE_CODE_FILE> -o <BINARY_FILE>
 
 To display the available subcommands that Unicorn has you can type `./target/debug/unicorn --help`, or to display subcommand options `./target/debug/unicorn <SUBCOMMAND> --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:
+
+<ol>
+    <li><a href="#beator">beator</a> to generate BTOR2 files.</li>
+    <li><a href="#quarc">quarc</a> to generate quantum circuits.</li>
+    <li><a href="#qubot">qubot</a> to generate QUBO/ISING models.</li>
+</ol>
+
+<h4 id="beator">1. Generate a BTOR2 file from a binary</h3>
+
 ```sh
 ./target/debug/unicorn beator <BINARY_FILE> --unroll <NUM_STATE_TRANSITIONS> --solver boolector --out <BTOR2_FILE>
 ```
 The above command generates a BTOR2 file, while the unroll option specifies how many state transitions Unicorn should represent in the BTOR2 file. In this example, Unicorn optimizes the number of variables using Boolector. 
 
 There are more options. For example, you can add `--bitblast` to the command, and the BTOR2 file will represent a logic (combinatorial) circuit.
 
+<h4 id="quarc"> 2. Quantum Circuits with QUARC </h4>
+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 <INPUT_FILE> --unroll <NUM_STATE_TRANSITIONS> --solver <SMT_SOLVER> --inputs <TEST_THESE_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!
+
+<h4 id="qubot"> 3. QUBOT </h4>
+Similarly, QUBOT can also build and test its models.
 
-### 2. Generate and/or test a QUBO of the binary
 ```sh
 ./target/debug/unicorn qubot <BINARY_FILE> --unroll <NUM_STATE_TRANSITIONS> --solver <SMT_SOLVER> --out <QUBO_FILE> --inputs 42,32;34
 ```

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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
+}

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;
+}

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;
+}

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;
+}

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;
+}