Add riscv example swap by Karl Palmskog

src/tools/symbexec/examples/riscv/Holmakefile.gen

@@ -0,0 +1,16 @@
+# includes
+# ----------------------------------
+DEPENDENCIES   = 
+
+
+# configuration
+# ----------------------------------
+HOLHEAP        = ../common/HolBATools_SymbExec_AnalysisCommon-heap
+NEWHOLHEAP     = 
+
+HEAPINC_EXTRA  = 
+
+
+# included lines follow
+# ----------------------------------
+include ../../../../Holmakefile.inc

src/tools/symbexec/examples/riscv/bin_rv_swapScript.sml

@@ -0,0 +1,26 @@
+open HolKernel Parse
+open PPBackEnd;
+
+open bir_inst_liftingLib;
+open bir_inst_liftingHelpersLib;
+open gcc_supportLib;
+
+val _ = Parse.current_backend := PPBackEnd.vt100_terminal;
+val _ = set_trace "bir_inst_lifting.DEBUG_LEVEL" 2;
+
+val _ = new_theory "bin_rv_swap";
+
+
+val dafilename = "swap.da";
+val prog_range = ((Arbnum.fromInt 0), (Arbnum.fromInt 0x20));
+
+val _ = print_with_style_ [Bold, Underline] ("Lifting "^dafilename^" (riscv)\n");
+
+val (region_map, sections) = read_disassembly_file_regions dafilename;
+val (thm, errors) = bmil_riscv.bir_lift_prog_gen prog_range sections;
+val _ = save_thm ("bin_rv_swap_thm", thm);
+
+val _ = print "\n\n";
+
+
+val _ = export_theory();

src/tools/symbexec/examples/riscv/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