Merge pull request #161 from kth-step/lifter-da-riscv

Parameterize DA lifter and add RISC-V tutorial

examples/riscv/README.md

@@ -0,0 +1,34 @@
+# Prerequisites for RISC-V examples 
+
+## Intalling the RISC-V cross-compilation toolchain
+
+Clone the RISC-V GNU Compiler Toolchain:
+
+```shell
+git clone https://github.com/riscv/riscv-gnu-toolchain
+```
+
+Install the prerequisites, e.g., on Ubuntu:
+
+```shell
+sudo apt-get install autoconf automake autotools-dev curl python3 python3-pip libmpc-dev libmpfr-dev libgmp-dev gawk build-essential bison flex texinfo gperf libtool patchutils bc zlib1g-dev libexpat-dev ninja-build git cmake libglib2.0-dev
+```
+
+Configure and build Linux cross-compiler:
+
+```shell
+./configure --prefix=/path/to/riscv
+make linux
+```
+
+## Installing and building HolBA
+
+To bootstrap Poly/ML, HOL4, and HolBA (may take tens of minutes):
+
+```shell
+git clone https://github.com/kth-step/HolBA.git
+cd HolBA
+./scripts/setup/install_all.sh
+./configure.sh
+make main
+```

examples/riscv/isqrt/Holmakefile.gen

@@ -0,0 +1,11 @@
+# configuration
+# ----------------------------------
+HOLHEAP        = ../../../src/HolBA-heap
+NEWHOLHEAP     = # TODO: Create a heap with lifted binaries
+
+HEAPINC_EXTRA  = 
+
+
+# included lines follow
+# ----------------------------------
+include ../../../src/Holmakefile.inc

examples/riscv/isqrt/README.md

@@ -0,0 +1,51 @@
+# RISC-V isqrt example
+
+## isqrt program
+
+We consider the following program which computes the
+integer square root of a given unsigned 64-bit integer.
+
+```c
+#include <stdint.h>
+
+uint64_t isqrt(uint64_t x) {
+  uint64_t y = 0;
+  while ((y+1)*(y+1) <= x) {
+    y += 1;
+  }
+  return y;
+}
+```
+
+## Compile and disassemble the isqrt program
+
+Compile `isqrt.c` as a library, producing `isqrt.o`:
+```shell
+/path/to/riscv/bin/riscv64-unknown-linux-gnu-gcc -std=gnu99 -Wall -fno-builtin -fno-stack-protector -march=rv64g -O1 -c -o isqrt.o isqrt.c
+```
+
+Compile `isqrt.c` to assembly, producing `isqrt.s` (optional):
+```shell
+/path/to/riscv/bin/riscv64-unknown-linux-gnu-gcc -std=gnu99 -Wall -fno-builtin -fno-stack-protector -march=rv64g -O1 -S -o isqrt.s isqrt.c
+```
+
+Disassemble `isqrt.o`, producing `isqrt.da`:
+```shell
+/path/to/riscv/bin/riscv64-unknown-linux-gnu-objdump -d isqrt.o
+```
+
+## Lifting the isqrt program to BIR
+
+The following command inside SML/HOL4 lifts the disassembled code to BIR:
+
+```sml
+val _ = lift_da_and_store "isqrt" "isqrt.da" ((Arbnum.fromInt 0), (Arbnum.fromInt 0x1000000));
+```
+
+## BIR isqrt program and its properties
+
+After lifting, the BIR program resides in the HOL4 term `bir_isqrt_prog`.
+The program's BIR statements can be obtained by:
+```sml
+val blocks = (fst o listSyntax.dest_list o dest_BirProgram o snd o dest_eq o concl o EVAL) ``bir_swap_prog``;
+```

examples/riscv/isqrt/isqrt.c

@@ -0,0 +1,9 @@
+#include <stdint.h>
+
+uint64_t isqrt(uint64_t x) {
+  uint64_t y = 0;
+  while ((y+1)*(y+1) <= x) {
+    y += 1;
+  }
+  return y;
+}

examples/riscv/isqrt/isqrt.da

@@ -0,0 +1,16 @@
+
+isqrt.o:     file format elf64-littleriscv
+
+
+Disassembly of section .text:
+
+0000000000000000 <isqrt>:
+   0:	00050693          	mv	a3,a0
+   4:	00000793          	li	a5,0
+
+0000000000000008 <.L2>:
+   8:	00078513          	mv	a0,a5
+   c:	00178793          	addi	a5,a5,1
+  10:	02f78733          	mul	a4,a5,a5
+  14:	fee6fae3          	bgeu	a3,a4,8 <.L2>
+  18:	00008067          	ret

examples/riscv/isqrt/isqrtScript.sml

@@ -0,0 +1,12 @@
+open HolKernel Parse;
+
+open bir_lifter_interfaceLib;
+
+val _ = Parse.current_backend := PPBackEnd.vt100_terminal;
+val _ = set_trace "bir_inst_lifting.DEBUG_LEVEL" 2;
+
+val _ = new_theory "isqrt";
+
+val _ = lift_da_and_store "isqrt" "isqrt.da" da_riscv ((Arbnum.fromInt 0), (Arbnum.fromInt 0x1000000));
+
+val _ = export_theory ();

examples/riscv/isqrt/isqrt_propScript.sml

@@ -0,0 +1,51 @@
+open HolKernel boolLib Parse bossLib;
+
+open BasicProvers simpLib metisLib;
+
+open logrootTheory arithmeticTheory pairTheory combinTheory wordsTheory;
+
+open bir_programSyntax bir_program_labelsTheory bir_immTheory;
+
+open isqrtTheory;
+
+val _ = new_theory "isqrt_prop";
+
+val blocks = (fst o listSyntax.dest_list o dest_BirProgram o snd o dest_eq o concl o EVAL) ``bir_isqrt_prog``;
+
+(el 1)blocks;
+(el 2)blocks;
+
+bir_isqrt_riscv_lift_THM;
+
+Definition SQRT_def:
+ SQRT x = ROOT 2 x
+End
+
+val arith_ss = srw_ss() ++ numSimps.old_ARITH_ss;
+
+Theorem sqrt_thm:
+!x p. SQRT x = let q = p * p in
+      if (q <= x /\ x < q + 2 * p + 1) then p else SQRT x
+Proof
+RW_TAC (arith_ss ++ boolSimps.LET_ss) [SQRT_def] THEN
+  MATCH_MP_TAC ROOT_UNIQUE THEN
+  RW_TAC bool_ss [ADD1,EXP_ADD,EXP_1,DECIDE ``2 = SUC 1``,
+    LEFT_ADD_DISTRIB,RIGHT_ADD_DISTRIB] THEN
+  DECIDE_TAC
+QED
+
+Definition wSQRT_def:
+ wSQRT w = n2w (SQRT (w2n w))
+End
+
+Definition isqrt_spec_def:
+ isqrt_spec_def ms ms' : bool =
+  let input = ms.c_gpr ms.procID 0w in
+  let output = ms'.c_gpr ms'.procID 0w in
+  output = wSQRT input
+End
+
+(* run symbolic execution of BIR to get two symbolic states  *)
+(* connect this back to the riscv state via the lifting theorem *)
+
+val _ = export_theory ();

examples/riscv/swap/Holmakefile.gen

@@ -0,0 +1,11 @@
+# configuration
+# ----------------------------------
+HOLHEAP        = ../../../src/HolBA-heap
+NEWHOLHEAP     = # TODO: Create a heap with lifted binaries
+
+HEAPINC_EXTRA  = 
+
+
+# included lines follow
+# ----------------------------------
+include ../../../src/Holmakefile.inc

examples/riscv/swap/README.md

@@ -0,0 +1,89 @@
+# RISC-V swap example
+
+## swap program
+
+We consider the following program which swaps the
+content of two given pointers to unsigned 64-bit integers.
+
+```c
+#include <stdint.h>
+
+void swap(uint64_t * x, uint64_t * y) {
+  uint64_t a, b;
+  a = * x;
+  b = * y;
+  if (a == b)
+    return;
+  * x = b;
+  * y = a;
+}
+```
+
+## Compile and disassemble the swap program
+
+Compile `swap.c` as a library, producing `swap.o`:
+```shell
+/path/to/riscv/bin/riscv64-unknown-linux-gnu-gcc -std=gnu99 -Wall -fno-builtin -fno-stack-protector -march=rv64g -O1 -c -o swap.o swap.c
+```
+
+Compile `swap.c` to assembly, producing `swap.s` (optional):
+```shell
+/path/to/riscv/bin/riscv64-unknown-linux-gnu-gcc -std=gnu99 -Wall -fno-builtin -fno-stack-protector -march=rv64g -O1 -S -o swap.s swap.c
+```
+
+Disassemble `swap.o`, producing `swap.da`:
+```shell
+/path/to/riscv/bin/riscv64-unknown-linux-gnu-objdump -d swap.o
+```
+
+## Lifting the swap program to BIR
+
+The following command inside SML/HOL4 lifts the disassembled code to BIR:
+
+```sml
+val _ = lift_da_and_store "swap" "swap.da" ((Arbnum.fromInt 0), (Arbnum.fromInt 0x1000000));
+```
+
+Parameters to the `lift_da_and_store` function are as follows:
+
+- `"swap"`: string representing the name of the HOL4 term that will be
+ defined to be equal to the translated BIR program
+- `"swap.da"`: path to the disassembled program
+- `((Arbnum.fromInt 0), (Arbnum.fromInt 0x1000000))`: superset of the
+  addresses that contains the program code. We call this memory region
+  `UnmodifiableMemory`.
+
+See `swapScript.sml` for the source code for the HOL4 theory that performs lifting.
+
+## BIR swap program and its properties
+
+After lifting, the BIR program resides in the HOL4 term `bir_swap_prog`.
+The program's BIR statements can be obtained by:
+
+```sml
+val blocks = (fst o listSyntax.dest_list o dest_BirProgram o snd o dest_eq o concl o EVAL) ``bir_swap_prog``;
+```
+
+Each block has a unique label (e.g., `BL_Address (Imm64 0w)`). In this
+case the label is an integer, which is equal to the address of the
+corresponding transpiled instruction. Labels can also be strings, for
+example when the block represents internal computations of an
+instruction or is generated by some program transformations (i.e. loop
+unrolling). A block has an internal list of statements, which are executed
+sequentially.
+
+Finally, a block always ends with a control flow statement. In this
+case, the block jumps to the next block, e.g., the block having label
+`BL_Address (Imm64 4w)`. Notice that it is not possible to jump to the
+middle of a block.
+
+`bir_swap_riscv_lift_THM` is the main theorem and states that the
+program has been correctly translated to BIR, and has this statement:
+```sml
+bir_is_lifted_prog riscv_bmr (WI_end 0w 0x1000000w) bir_swap_progbin bir_swap_prog
+```
+
+See the definition of `bir_is_lifted_prog` for what the theorem means:
+```
+DB.find "bir_is_lifted_prog_def";
+```

examples/riscv/swap/swap.c

@@ -0,0 +1,11 @@
+#include <stdint.h>
+
+void swap(uint64_t * x, uint64_t * y) {
+  uint64_t a, b;
+  a = * x;
+  b = * y;
+  if (a == b)
+    return;
+  * x = b;
+  * y = a;
+}

examples/riscv/swap/swap.da

@@ -0,0 +1,15 @@
+
+swap.o:     file format elf64-littleriscv
+
+
+Disassembly of section .text:
+
+0000000000000000 <swap>:
+   0:	00053783          	ld	a5,0(a0)
+   4:	0005b703          	ld	a4,0(a1)
+   8:	00e78663          	beq	a5,a4,14 <.L1>
+   c:	00e53023          	sd	a4,0(a0)
+  10:	00f5b023          	sd	a5,0(a1)
+
+0000000000000014 <.L1>:
+  14:	00008067          	ret

examples/riscv/swap/swapScript.sml

@@ -0,0 +1,12 @@
+open HolKernel Parse;
+
+open bir_lifter_interfaceLib;
+
+val _ = Parse.current_backend := PPBackEnd.vt100_terminal;
+val _ = set_trace "bir_inst_lifting.DEBUG_LEVEL" 2;
+
+val _ = new_theory "swap";
+
+val _ = lift_da_and_store "swap" "swap.da" da_riscv ((Arbnum.fromInt 0), (Arbnum.fromInt 0x1000000));
+
+val _ = export_theory ();

examples/riscv/swap/swap_concrete_execScript.sml

@@ -0,0 +1,9 @@
+open HolKernel Parse;
+
+open bir_exec_envLib;
+open bir_execLib;
+open swapTheory;
+
+val _ = new_theory "swap_concrete_exec";
+
+val _ = export_theory ();

examples/riscv/swap/swap_propScript.sml

@@ -0,0 +1,36 @@
+open HolKernel boolLib Parse bossLib;
+
+open bir_programSyntax bir_program_labelsTheory bir_immTheory;
+
+open swapTheory;
+
+val _ = new_theory "swap_prop";
+
+val blocks = (fst o listSyntax.dest_list o dest_BirProgram o snd o dest_eq o concl o EVAL) ``bir_swap_prog``;
+
+(el 1)blocks;
+(el 2)blocks;
+
+bir_swap_riscv_lift_THM;
+
+Definition swap_mem_spec_def:
+ swap_mem_spec ms =
+ let ms'_mem8 = (riscv_mem_store_word (ms.c_gpr ms.procID 0w)
+   (riscv_mem_load_word ms.MEM8 (ms.c_gpr ms.procID 1w)) ms.MEM8)
+ in
+   (riscv_mem_store_word (ms.c_gpr ms.procID 1w)
+    (riscv_mem_load_word ms.MEM8 (ms.c_gpr ms.procID 0w)) ms'_mem8)
+End
+
+Definition swap_spec_output_def:
+ swap_spec_output ms : riscv_state = ms with MEM8 := swap_mem_spec ms
+End
+
+Definition swap_spec_def:
+ swap_spec ms ms' : bool = (ms'.MEM8 = swap_mem_spec ms)
+End
+
+(* run symbolic execution of BIR to get two symbolic states  *)
+(* connect this back to the riscv state via the lifting theorem *)
+
+val _ = export_theory ();

examples/tutorial/2-lift/bir_prog_add_regScript.sml

@@ -10,6 +10,7 @@ val _ = new_theory "bir_prog_add_reg";
 
 val _ = lift_da_and_store "add_reg"
                           "../1-code/src/add_reg.da"
+                          da_arm8
                           ((Arbnum.fromInt 0), (Arbnum.fromInt 0x1000000));
 
 val _ = export_theory();

src/tools/lifter/bir_lifter_interfaceLib.sig

@@ -0,0 +1,10 @@
+signature bir_lifter_interfaceLib =
+sig
+
+  datatype da_isa =
+    da_arm8
+  | da_riscv
+
+  val lift_da_and_store : string -> string -> da_isa -> Arbnum.num * Arbnum.num -> unit;
+
+end