isqrt lifting example, fix other riscv example issues

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.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" ((Arbnum.fromInt 0), (Arbnum.fromInt 0x1000000));
+
+val _ = export_theory ();

examples/riscv/isqrt/isqrt_propScript.sml

@@ -0,0 +1,34 @@
+open HolKernel boolLib Parse bossLib;
+
+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 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_def:
+ swap_spec ms = ms with 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/riscv/swap/README.md

@@ -2,6 +2,9 @@
 
 ## swap program
 
+We consider the following program which swaps the
+content of two given pointers to unsigned 64-bit integers.
+
 ```c
 #include <stdint.h>
 
@@ -16,7 +19,7 @@ void swap(uint64_t * x, uint64_t * y) {
 }
 ```
 
-## Compile and disassemble swap program
+## Compile and disassemble the swap program
 
 Compile `swap.c` as a library, producing `swap.o`:
 ```shell
@@ -33,7 +36,7 @@ Disassemble `swap.o`, producing `swap.da`:
 /path/to/riscv/bin/riscv64-unknown-linux-gnu-objdump -d swap.o
 ```
 
-## Lifting swap library to BIR
+## Lifting the swap program to BIR
 
 The following command inside SML/HOL4 lifts the disassembled code to BIR:
 

examples/riscv/swap/swapScript.sml

@@ -7,6 +7,6 @@ val _ = set_trace "bir_inst_lifting.DEBUG_LEVEL" 2;
 
 val _ = new_theory "swap";
 
-val _ = lift_da_and_store "swap" "swapO1.da" ((Arbnum.fromInt 0), (Arbnum.fromInt 0x1000000));
+val _ = lift_da_and_store "swap" "swap.da" ((Arbnum.fromInt 0), (Arbnum.fromInt 0x1000000));
 
 val _ = export_theory ();