linked version of swap riscv example, fix riscv tests

kth-step · Jul 4, 2024 · a3bec1a · a3bec1a
1 parent 4c7fde8
commit a3bec1a
Show file tree

Hide file tree

Showing 7 changed files with 36 additions and 23 deletions.
diff --git a/examples/riscv/common/bir_symbLib.sml b/examples/riscv/common/bir_symbLib.sml
@@ -12,13 +12,17 @@ local
   open birs_auxTheory;
 in
 
+val prog_addr_max_tm = ``0x20000w:word64``;
+
+val mem_addr_bound_tm = ``0x100000000w:word64``;
+
 fun mem_addrs_prog_disj_bir_tm rn = ``BExp_BinExp BIExp_And
  (BExp_BinPred BIExp_LessOrEqual
-  (BExp_Const (Imm64 0x1000w))
+  (BExp_Const (Imm64 ^prog_addr_max_tm))
   (BExp_Den (BVar ^(stringSyntax.fromMLstring rn) (BType_Imm Bit64))))
  (BExp_BinPred BIExp_LessThan
   (BExp_Den (BVar ^(stringSyntax.fromMLstring rn) (BType_Imm Bit64)))
-  (BExp_Const (Imm64 0x100000000w)))``;
+  (BExp_Const (Imm64 ^mem_addr_bound_tm)))``;
 
 fun mem_addrs_aligned_prog_disj_bir_tm rn = ``BExp_BinExp BIExp_And
   (BExp_Aligned Bit64 3 (BExp_Den (BVar ^(stringSyntax.fromMLstring rn) (BType_Imm Bit64))))
@@ -28,7 +32,7 @@ fun mem_addrs_aligned_prog_disj_riscv_tm vn =
  let
    val var_tm = mk_var (vn, wordsSyntax.mk_int_word_type 64)
  in
-  ``^var_tm && 7w = 0w /\ 0x1000w <=+ ^var_tm /\ ^var_tm <+ 0x100000000w``
+  ``^var_tm && 7w = 0w /\ ^prog_addr_max_tm <=+ ^var_tm /\ ^var_tm <+ ^mem_addr_bound_tm``
  end;
 
 fun pre_vals_reg_bir_tm rn fv = Parse.Term (`

diff --git a/examples/riscv/riscv-spec.pdf b/examples/riscv/riscv-spec.pdf
diff --git a/examples/riscv/swap/swap.c b/examples/riscv/swap/swap.c
@@ -9,3 +9,10 @@ void swap(uint64_t * x, uint64_t * y) {
   * x = b;
   * y = a;
 }
+
+int main(void) {
+  uint64_t a = 1;
+  uint64_t b = 0;
+  swap(&a, &b);
+  return a;
+}
diff --git a/examples/riscv/swap/swap.da b/examples/riscv/swap/swap.da
@@ -4,12 +4,14 @@ 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
+0000000000010488 <swap>:
+   10488:	00053783          	ld	a5,0(a0)
+   1048c:	0005b703          	ld	a4,0(a1)
+   10490:	00e78663          	beq	a5,a4,1049c <swap+0x14>
+   10494:	00e53023          	sd	a4,0(a0)
+   10498:	00f5b023          	sd	a5,0(a1)
+   1049c:	00008067          	ret
+
+00000000000104a0 <main>:
+   104a0:	00000513          	li	a0,0
+   104a4:	00008067          	ret
diff --git a/examples/riscv/swap/swapScript.sml b/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" "swap.da" da_riscv ((Arbnum.fromInt 0), (Arbnum.fromInt 0x20));
+val _ = lift_da_and_store "swap" "swap.da" da_riscv ((Arbnum.fromInt 0x10488), (Arbnum.fromInt 0x104a6));
 
 val _ = export_theory ();
diff --git a/examples/riscv/swap/swap_specScript.sml b/examples/riscv/swap/swap_specScript.sml
@@ -54,11 +54,11 @@ val _ = new_theory "swap_spec";
 (* ------------------ *)
 
 Definition swap_init_addr_def:
- swap_init_addr : word64 = 0x00w
+ swap_init_addr : word64 = 0x10488w
 End
 
 Definition swap_end_addr_def:
- swap_end_addr : word64 = 0x14w
+ swap_end_addr : word64 = 0x1049cw
 End
 
 (* --------------- *)

diff --git a/examples/riscv/test-riscv.sml b/examples/riscv/test-riscv.sml
@@ -31,7 +31,7 @@ val _ = print_and_check_thm
   "swap RISC-V lift theorem"
   bir_swap_riscv_lift_THM
   ``
-  bir_is_lifted_prog riscv_bmr (WI_end (0w : word64) (32w : word64))
+  bir_is_lifted_prog riscv_bmr (WI_end (0x10488w : word64) (0x104A6w : word64))
    bir_swap_progbin
    (bir_swap_prog : 'observation_type bir_program_t)
   ``;
@@ -40,10 +40,10 @@ val _ = print_and_check_thm
   "swap BSPEC contract theorem"
   bspec_cont_swap
   ``bir_cont (bir_swap_prog : 'a bir_program_t)
-    bir_exp_true (BL_Address (Imm64 0x00w))
-    {BL_Address (Imm64 0x14w)} {}
+    bir_exp_true (BL_Address (Imm64 0x10488w))
+    {BL_Address (Imm64 0x1049cw)} {}
     (bspec_swap_pre pre_x10 pre_x11 pre_x10_deref pre_x11_deref)
-    (\l. if l = BL_Address (Imm64 0x14w)
+    (\l. if l = BL_Address (Imm64 0x1049cw)
          then bspec_swap_post pre_x10 pre_x11 pre_x10_deref pre_x11_deref
          else bir_exp_false)
   ``;
@@ -65,7 +65,7 @@ val _ = print_and_check_thm
   "incr RISC-V lift theorem"
   bir_incr_riscv_lift_THM
   ``
-  bir_is_lifted_prog riscv_bmr (WI_end (0w : word64) (8w : word64))
+  bir_is_lifted_prog riscv_bmr (WI_end (0x10488w : word64) (0x10495w : word64))
    bir_incr_progbin
    (bir_incr_prog : 'observation_type bir_program_t)
   ``;
@@ -74,9 +74,9 @@ val _ = print_and_check_thm
   "incr BSPEC contract theorem"
   bspec_cont_incr
  ``bir_cont (bir_incr_prog : 'a bir_program_t)
-  bir_exp_true (BL_Address (Imm64 0w))
-  {BL_Address (Imm64 4w)} {} (bspec_incr_pre pre_x10)
-  (\l. if l = BL_Address (Imm64 4w)
+  bir_exp_true (BL_Address (Imm64 0x10488w))
+  {BL_Address (Imm64 0x1048cw)} {} (bspec_incr_pre pre_x10)
+  (\l. if l = BL_Address (Imm64 0x1048cw)
        then bspec_incr_post pre_x10
        else bir_exp_false)``;