use riscv when lifting in interface

examples/riscv/swap/README.md

@@ -21,12 +21,12 @@ void swap(uint64_t * x, uint64_t * y) {
 Compile `swap.c` as a library, producing `swap.o`:
 
 ```shell
-/path/to/riscv/bin/riscv64-unknown-linux-gnu-gcc -fno-stack-protector -c -o swap.o -O0 swap.c
+/path/to/riscv/bin/riscv64-unknown-linux-gnu-gcc -std=gnu99 -Wall -fno-builtin -fno-stack-protector -march=rv64g -O0 -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 -fno-stack-protector -O0 -S -o swap.s swap.c
+/path/to/riscv/bin/riscv64-unknown-linux-gnu-gcc -std=gnu99 -Wall -fno-builtin -fno-stack-protector -march=rv64g -O0 -S -o swap.s swap.c
 ```
 
 Disassemble `swap.o`, producing `swap.da`:

examples/riscv/swap/swap.da

@@ -0,0 +1,36 @@
+
+swap.o:     file format elf64-littleriscv
+
+
+Disassembly of section .text:
+
+0000000000000000 <swap>:
+   0:	fd010113          	addi	sp,sp,-48
+   4:	02813423          	sd	s0,40(sp)
+   8:	03010413          	addi	s0,sp,48
+   c:	fca43c23          	sd	a0,-40(s0)
+  10:	fcb43823          	sd	a1,-48(s0)
+  14:	fd843783          	ld	a5,-40(s0)
+  18:	0007b783          	ld	a5,0(a5)
+  1c:	fef43423          	sd	a5,-24(s0)
+  20:	fd043783          	ld	a5,-48(s0)
+  24:	0007b783          	ld	a5,0(a5)
+  28:	fef43023          	sd	a5,-32(s0)
+  2c:	fe843703          	ld	a4,-24(s0)
+  30:	fe043783          	ld	a5,-32(s0)
+  34:	02f70063          	beq	a4,a5,54 <.L4>
+  38:	fd843783          	ld	a5,-40(s0)
+  3c:	fe043703          	ld	a4,-32(s0)
+  40:	00e7b023          	sd	a4,0(a5)
+  44:	fd043783          	ld	a5,-48(s0)
+  48:	fe843703          	ld	a4,-24(s0)
+  4c:	00e7b023          	sd	a4,0(a5)
+  50:	0080006f          	j	58 <.L1>
+
+0000000000000054 <.L4>:
+  54:	00000013          	nop
+
+0000000000000058 <.L1>:
+  58:	02813403          	ld	s0,40(sp)
+  5c:	03010113          	addi	sp,sp,48
+  60:	00008067          	ret

src/tools/lifter/bir_lifter_interfaceLib.sml

@@ -42,11 +42,11 @@ fun lift_da_and_store prog_name da_name prog_interval =
 
     val (region_map, aes_sections) = read_disassembly_file_regions da_name
 
-    val (thm_arm8, errors) = bmil_arm8.bir_lift_prog_gen
+    val (thm_riscv, errors) = bmil_riscv.bir_lift_prog_gen
 			       prog_interval
 			       aes_sections
 
-    val (lift_app_1_tm, bir_prog_tm) = (dest_comb o concl) thm_arm8;
+    val (lift_app_1_tm, bir_prog_tm) = (dest_comb o concl) thm_riscv;
     val (_, bir_progbin_tm) = dest_comb lift_app_1_tm;
 
     val _ = print "\n\n";
@@ -58,9 +58,9 @@ fun lift_da_and_store prog_name da_name prog_interval =
     val bir_x_progbin_def = Define `^bir_x_progbin_var = ^bir_progbin_tm`;
 
     (* now save the lifter theorem using the definitions *)
-    val bir_x_arm8_lift_THM = save_thm ("bir_"^prog_name^"_arm8_lift_THM",
+    val bir_x_riscv_lift_THM = save_thm ("bir_"^prog_name^"_riscv_lift_THM",
 	   REWRITE_RULE [GSYM bir_x_prog_def,
-			 GSYM bir_x_progbin_def] thm_arm8);
+			 GSYM bir_x_progbin_def] thm_riscv);
   in
     ()
   end;