From 3dafdd006e1dce5d54de6ff2bb93fe9c63aaf103 Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Fri, 19 Apr 2024 15:23:17 +0100 Subject: [PATCH] Changes from updating the RISC-V model --- instructions/binary_search_riscv64/a10.v | 17 ++++++++--------- instructions/binary_search_riscv64/a14.v | 17 ++++++++--------- instructions/binary_search_riscv64/a18.v | 17 ++++++++--------- instructions/binary_search_riscv64/a1c.v | 17 ++++++++--------- instructions/binary_search_riscv64/a4.v | 17 ++++++++--------- instructions/binary_search_riscv64/a58.v | 17 ++++++++--------- instructions/binary_search_riscv64/a7c.v | 17 ++++++++--------- instructions/binary_search_riscv64/a8.v | 17 ++++++++--------- instructions/binary_search_riscv64/a80.v | 17 ++++++++--------- instructions/binary_search_riscv64/a84.v | 17 ++++++++--------- instructions/binary_search_riscv64/a88.v | 17 ++++++++--------- instructions/binary_search_riscv64/a8c.v | 17 ++++++++--------- instructions/binary_search_riscv64/a90.v | 17 ++++++++--------- instructions/binary_search_riscv64/a94.v | 17 ++++++++--------- instructions/binary_search_riscv64/ac.v | 17 ++++++++--------- instructions/memcpy_riscv64/a4.v | 17 ++++++++--------- instructions/memcpy_riscv64/a8.v | 19 +++++++++---------- instructions/riscv64_test/a8.v | 17 ++++++++--------- instructions/riscv64_test/ac.v | 17 ++++++++--------- theories/riscv64/sys_regs.v | 2 ++ 20 files changed, 155 insertions(+), 172 deletions(-) diff --git a/instructions/binary_search_riscv64/a10.v b/instructions/binary_search_riscv64/a10.v index 0abcd68..2a8abbb 100644 --- a/instructions/binary_search_riscv64/a10.v +++ b/instructions/binary_search_riscv64/a10.v @@ -1,7 +1,7 @@ From isla Require Import opsem. Definition a10 : isla_trace := - AssumeReg "rv_enable_pmp" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: + AssumeReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: AssumeReg "rv_enable_misaligned_access" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: AssumeReg "rv_ram_base" [] (RegVal_Base (Val_Bits (BV 64%N 0x80000000%Z))) Mk_annot :t: AssumeReg "rv_ram_size" [] (RegVal_Base (Val_Bits (BV 64%N 0x4000000%Z))) Mk_annot :t: @@ -27,14 +27,13 @@ Definition a10 : isla_trace := Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x20%Z)) Mk_annot] Mk_annot)) Mk_annot :t: ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t: ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t: - Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t: - Smt (DeclareConst 25%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadReg "x18" [] (RegVal_Base (Val_Symbolic 25%Z)) Mk_annot :t: - Smt (DefineConst 28%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DefineConst 34%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DeclareConst 38%Z Ty_Bool) Mk_annot :t: - WriteMem (RegVal_Base (Val_Symbolic 38%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) (RegVal_Base (Val_Symbolic 25%Z)) 8%N None Mk_annot :t: + Smt (DeclareConst 17%Z (Ty_BitVec 64%N)) Mk_annot :t: + ReadReg "x18" [] (RegVal_Base (Val_Symbolic 17%Z)) Mk_annot :t: + ReadReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: + Smt (DefineConst 20%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DefineConst 26%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DeclareConst 30%Z Ty_Bool) Mk_annot :t: + WriteMem (RegVal_Base (Val_Symbolic 30%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) (RegVal_Base (Val_Symbolic 17%Z)) 8%N None Mk_annot :t: WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t: tnil . diff --git a/instructions/binary_search_riscv64/a14.v b/instructions/binary_search_riscv64/a14.v index 7e2d7b6..ea3abcc 100644 --- a/instructions/binary_search_riscv64/a14.v +++ b/instructions/binary_search_riscv64/a14.v @@ -1,7 +1,7 @@ From isla Require Import opsem. Definition a14 : isla_trace := - AssumeReg "rv_enable_pmp" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: + AssumeReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: AssumeReg "rv_enable_misaligned_access" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: AssumeReg "rv_ram_base" [] (RegVal_Base (Val_Bits (BV 64%N 0x80000000%Z))) Mk_annot :t: AssumeReg "rv_ram_size" [] (RegVal_Base (Val_Bits (BV 64%N 0x4000000%Z))) Mk_annot :t: @@ -27,14 +27,13 @@ Definition a14 : isla_trace := Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x18%Z)) Mk_annot] Mk_annot)) Mk_annot :t: ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t: ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t: - Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t: - Smt (DeclareConst 25%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadReg "x19" [] (RegVal_Base (Val_Symbolic 25%Z)) Mk_annot :t: - Smt (DefineConst 28%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DefineConst 34%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DeclareConst 38%Z Ty_Bool) Mk_annot :t: - WriteMem (RegVal_Base (Val_Symbolic 38%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) (RegVal_Base (Val_Symbolic 25%Z)) 8%N None Mk_annot :t: + Smt (DeclareConst 17%Z (Ty_BitVec 64%N)) Mk_annot :t: + ReadReg "x19" [] (RegVal_Base (Val_Symbolic 17%Z)) Mk_annot :t: + ReadReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: + Smt (DefineConst 20%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DefineConst 26%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DeclareConst 30%Z Ty_Bool) Mk_annot :t: + WriteMem (RegVal_Base (Val_Symbolic 30%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) (RegVal_Base (Val_Symbolic 17%Z)) 8%N None Mk_annot :t: WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t: tnil . diff --git a/instructions/binary_search_riscv64/a18.v b/instructions/binary_search_riscv64/a18.v index 6d6f5b6..34d9356 100644 --- a/instructions/binary_search_riscv64/a18.v +++ b/instructions/binary_search_riscv64/a18.v @@ -1,7 +1,7 @@ From isla Require Import opsem. Definition a18 : isla_trace := - AssumeReg "rv_enable_pmp" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: + AssumeReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: AssumeReg "rv_enable_misaligned_access" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: AssumeReg "rv_ram_base" [] (RegVal_Base (Val_Bits (BV 64%N 0x80000000%Z))) Mk_annot :t: AssumeReg "rv_ram_size" [] (RegVal_Base (Val_Bits (BV 64%N 0x4000000%Z))) Mk_annot :t: @@ -27,14 +27,13 @@ Definition a18 : isla_trace := Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x10%Z)) Mk_annot] Mk_annot)) Mk_annot :t: ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t: ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t: - Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t: - Smt (DeclareConst 25%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadReg "x20" [] (RegVal_Base (Val_Symbolic 25%Z)) Mk_annot :t: - Smt (DefineConst 28%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DefineConst 34%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DeclareConst 38%Z Ty_Bool) Mk_annot :t: - WriteMem (RegVal_Base (Val_Symbolic 38%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) (RegVal_Base (Val_Symbolic 25%Z)) 8%N None Mk_annot :t: + Smt (DeclareConst 17%Z (Ty_BitVec 64%N)) Mk_annot :t: + ReadReg "x20" [] (RegVal_Base (Val_Symbolic 17%Z)) Mk_annot :t: + ReadReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: + Smt (DefineConst 20%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DefineConst 26%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DeclareConst 30%Z Ty_Bool) Mk_annot :t: + WriteMem (RegVal_Base (Val_Symbolic 30%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) (RegVal_Base (Val_Symbolic 17%Z)) 8%N None Mk_annot :t: WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t: tnil . diff --git a/instructions/binary_search_riscv64/a1c.v b/instructions/binary_search_riscv64/a1c.v index 47eabdc..a301f6b 100644 --- a/instructions/binary_search_riscv64/a1c.v +++ b/instructions/binary_search_riscv64/a1c.v @@ -1,7 +1,7 @@ From isla Require Import opsem. Definition a1c : isla_trace := - AssumeReg "rv_enable_pmp" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: + AssumeReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: AssumeReg "rv_enable_misaligned_access" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: AssumeReg "rv_ram_base" [] (RegVal_Base (Val_Bits (BV 64%N 0x80000000%Z))) Mk_annot :t: AssumeReg "rv_ram_size" [] (RegVal_Base (Val_Bits (BV 64%N 0x4000000%Z))) Mk_annot :t: @@ -27,14 +27,13 @@ Definition a1c : isla_trace := Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x8%Z)) Mk_annot] Mk_annot)) Mk_annot :t: ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t: ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t: - Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t: - Smt (DeclareConst 25%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadReg "x21" [] (RegVal_Base (Val_Symbolic 25%Z)) Mk_annot :t: - Smt (DefineConst 28%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DefineConst 34%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DeclareConst 38%Z Ty_Bool) Mk_annot :t: - WriteMem (RegVal_Base (Val_Symbolic 38%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) (RegVal_Base (Val_Symbolic 25%Z)) 8%N None Mk_annot :t: + Smt (DeclareConst 17%Z (Ty_BitVec 64%N)) Mk_annot :t: + ReadReg "x21" [] (RegVal_Base (Val_Symbolic 17%Z)) Mk_annot :t: + ReadReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: + Smt (DefineConst 20%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DefineConst 26%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DeclareConst 30%Z Ty_Bool) Mk_annot :t: + WriteMem (RegVal_Base (Val_Symbolic 30%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) (RegVal_Base (Val_Symbolic 17%Z)) 8%N None Mk_annot :t: WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t: tnil . diff --git a/instructions/binary_search_riscv64/a4.v b/instructions/binary_search_riscv64/a4.v index 8b10427..f482cc6 100644 --- a/instructions/binary_search_riscv64/a4.v +++ b/instructions/binary_search_riscv64/a4.v @@ -1,7 +1,7 @@ From isla Require Import opsem. Definition a4 : isla_trace := - AssumeReg "rv_enable_pmp" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: + AssumeReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: AssumeReg "rv_enable_misaligned_access" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: AssumeReg "rv_ram_base" [] (RegVal_Base (Val_Bits (BV 64%N 0x80000000%Z))) Mk_annot :t: AssumeReg "rv_ram_size" [] (RegVal_Base (Val_Bits (BV 64%N 0x4000000%Z))) Mk_annot :t: @@ -27,14 +27,13 @@ Definition a4 : isla_trace := Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x38%Z)) Mk_annot] Mk_annot)) Mk_annot :t: ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t: ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t: - Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t: - Smt (DeclareConst 25%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadReg "x1" [] (RegVal_Base (Val_Symbolic 25%Z)) Mk_annot :t: - Smt (DefineConst 28%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DefineConst 34%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DeclareConst 38%Z Ty_Bool) Mk_annot :t: - WriteMem (RegVal_Base (Val_Symbolic 38%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) (RegVal_Base (Val_Symbolic 25%Z)) 8%N None Mk_annot :t: + Smt (DeclareConst 17%Z (Ty_BitVec 64%N)) Mk_annot :t: + ReadReg "x1" [] (RegVal_Base (Val_Symbolic 17%Z)) Mk_annot :t: + ReadReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: + Smt (DefineConst 20%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DefineConst 26%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DeclareConst 30%Z Ty_Bool) Mk_annot :t: + WriteMem (RegVal_Base (Val_Symbolic 30%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) (RegVal_Base (Val_Symbolic 17%Z)) 8%N None Mk_annot :t: WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t: tnil . diff --git a/instructions/binary_search_riscv64/a58.v b/instructions/binary_search_riscv64/a58.v index 56d6693..b18cf2c 100644 --- a/instructions/binary_search_riscv64/a58.v +++ b/instructions/binary_search_riscv64/a58.v @@ -1,7 +1,7 @@ From isla Require Import opsem. Definition a58 : isla_trace := - AssumeReg "rv_enable_pmp" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: + AssumeReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: AssumeReg "rv_enable_misaligned_access" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: AssumeReg "rv_ram_base" [] (RegVal_Base (Val_Bits (BV 64%N 0x80000000%Z))) Mk_annot :t: AssumeReg "rv_ram_size" [] (RegVal_Base (Val_Bits (BV 64%N 0x4000000%Z))) Mk_annot :t: @@ -27,14 +27,13 @@ Definition a58 : isla_trace := Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t: ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t: ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t: - Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t: - Smt (DefineConst 27%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DefineConst 33%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DeclareConst 37%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadMem (RegVal_Base (Val_Symbolic 37%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) 8%N None Mk_annot :t: - Smt (DefineConst 38%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 37%Z) Mk_annot) Mk_annot)) Mk_annot :t: - WriteReg "x10" [] (RegVal_Base (Val_Symbolic 38%Z)) Mk_annot :t: + ReadReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: + Smt (DefineConst 19%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DefineConst 25%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DeclareConst 29%Z (Ty_BitVec 64%N)) Mk_annot :t: + ReadMem (RegVal_Base (Val_Symbolic 29%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) 8%N None Mk_annot :t: + Smt (DefineConst 30%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 29%Z) Mk_annot) Mk_annot)) Mk_annot :t: + WriteReg "x10" [] (RegVal_Base (Val_Symbolic 30%Z)) Mk_annot :t: WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t: tnil . diff --git a/instructions/binary_search_riscv64/a7c.v b/instructions/binary_search_riscv64/a7c.v index 15c2414..c839175 100644 --- a/instructions/binary_search_riscv64/a7c.v +++ b/instructions/binary_search_riscv64/a7c.v @@ -1,7 +1,7 @@ From isla Require Import opsem. Definition a7c : isla_trace := - AssumeReg "rv_enable_pmp" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: + AssumeReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: AssumeReg "rv_enable_misaligned_access" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: AssumeReg "rv_ram_base" [] (RegVal_Base (Val_Bits (BV 64%N 0x80000000%Z))) Mk_annot :t: AssumeReg "rv_ram_size" [] (RegVal_Base (Val_Bits (BV 64%N 0x4000000%Z))) Mk_annot :t: @@ -27,14 +27,13 @@ Definition a7c : isla_trace := Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x8%Z)) Mk_annot] Mk_annot)) Mk_annot :t: ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t: ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t: - Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t: - Smt (DefineConst 27%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DefineConst 33%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DeclareConst 37%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadMem (RegVal_Base (Val_Symbolic 37%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) 8%N None Mk_annot :t: - Smt (DefineConst 38%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 37%Z) Mk_annot) Mk_annot)) Mk_annot :t: - WriteReg "x21" [] (RegVal_Base (Val_Symbolic 38%Z)) Mk_annot :t: + ReadReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: + Smt (DefineConst 19%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DefineConst 25%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DeclareConst 29%Z (Ty_BitVec 64%N)) Mk_annot :t: + ReadMem (RegVal_Base (Val_Symbolic 29%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) 8%N None Mk_annot :t: + Smt (DefineConst 30%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 29%Z) Mk_annot) Mk_annot)) Mk_annot :t: + WriteReg "x21" [] (RegVal_Base (Val_Symbolic 30%Z)) Mk_annot :t: WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t: tnil . diff --git a/instructions/binary_search_riscv64/a8.v b/instructions/binary_search_riscv64/a8.v index 77349f0..1284994 100644 --- a/instructions/binary_search_riscv64/a8.v +++ b/instructions/binary_search_riscv64/a8.v @@ -1,7 +1,7 @@ From isla Require Import opsem. Definition a8 : isla_trace := - AssumeReg "rv_enable_pmp" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: + AssumeReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: AssumeReg "rv_enable_misaligned_access" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: AssumeReg "rv_ram_base" [] (RegVal_Base (Val_Bits (BV 64%N 0x80000000%Z))) Mk_annot :t: AssumeReg "rv_ram_size" [] (RegVal_Base (Val_Bits (BV 64%N 0x4000000%Z))) Mk_annot :t: @@ -27,14 +27,13 @@ Definition a8 : isla_trace := Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x30%Z)) Mk_annot] Mk_annot)) Mk_annot :t: ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t: ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t: - Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t: - Smt (DeclareConst 25%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadReg "x8" [] (RegVal_Base (Val_Symbolic 25%Z)) Mk_annot :t: - Smt (DefineConst 28%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DefineConst 34%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DeclareConst 38%Z Ty_Bool) Mk_annot :t: - WriteMem (RegVal_Base (Val_Symbolic 38%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) (RegVal_Base (Val_Symbolic 25%Z)) 8%N None Mk_annot :t: + Smt (DeclareConst 17%Z (Ty_BitVec 64%N)) Mk_annot :t: + ReadReg "x8" [] (RegVal_Base (Val_Symbolic 17%Z)) Mk_annot :t: + ReadReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: + Smt (DefineConst 20%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DefineConst 26%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DeclareConst 30%Z Ty_Bool) Mk_annot :t: + WriteMem (RegVal_Base (Val_Symbolic 30%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) (RegVal_Base (Val_Symbolic 17%Z)) 8%N None Mk_annot :t: WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t: tnil . diff --git a/instructions/binary_search_riscv64/a80.v b/instructions/binary_search_riscv64/a80.v index 7e8c4ab..9a254d1 100644 --- a/instructions/binary_search_riscv64/a80.v +++ b/instructions/binary_search_riscv64/a80.v @@ -1,7 +1,7 @@ From isla Require Import opsem. Definition a80 : isla_trace := - AssumeReg "rv_enable_pmp" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: + AssumeReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: AssumeReg "rv_enable_misaligned_access" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: AssumeReg "rv_ram_base" [] (RegVal_Base (Val_Bits (BV 64%N 0x80000000%Z))) Mk_annot :t: AssumeReg "rv_ram_size" [] (RegVal_Base (Val_Bits (BV 64%N 0x4000000%Z))) Mk_annot :t: @@ -27,14 +27,13 @@ Definition a80 : isla_trace := Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x10%Z)) Mk_annot] Mk_annot)) Mk_annot :t: ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t: ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t: - Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t: - Smt (DefineConst 27%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DefineConst 33%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DeclareConst 37%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadMem (RegVal_Base (Val_Symbolic 37%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) 8%N None Mk_annot :t: - Smt (DefineConst 38%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 37%Z) Mk_annot) Mk_annot)) Mk_annot :t: - WriteReg "x20" [] (RegVal_Base (Val_Symbolic 38%Z)) Mk_annot :t: + ReadReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: + Smt (DefineConst 19%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DefineConst 25%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DeclareConst 29%Z (Ty_BitVec 64%N)) Mk_annot :t: + ReadMem (RegVal_Base (Val_Symbolic 29%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) 8%N None Mk_annot :t: + Smt (DefineConst 30%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 29%Z) Mk_annot) Mk_annot)) Mk_annot :t: + WriteReg "x20" [] (RegVal_Base (Val_Symbolic 30%Z)) Mk_annot :t: WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t: tnil . diff --git a/instructions/binary_search_riscv64/a84.v b/instructions/binary_search_riscv64/a84.v index 0d73268..bcfd00b 100644 --- a/instructions/binary_search_riscv64/a84.v +++ b/instructions/binary_search_riscv64/a84.v @@ -1,7 +1,7 @@ From isla Require Import opsem. Definition a84 : isla_trace := - AssumeReg "rv_enable_pmp" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: + AssumeReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: AssumeReg "rv_enable_misaligned_access" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: AssumeReg "rv_ram_base" [] (RegVal_Base (Val_Bits (BV 64%N 0x80000000%Z))) Mk_annot :t: AssumeReg "rv_ram_size" [] (RegVal_Base (Val_Bits (BV 64%N 0x4000000%Z))) Mk_annot :t: @@ -27,14 +27,13 @@ Definition a84 : isla_trace := Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x18%Z)) Mk_annot] Mk_annot)) Mk_annot :t: ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t: ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t: - Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t: - Smt (DefineConst 27%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DefineConst 33%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DeclareConst 37%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadMem (RegVal_Base (Val_Symbolic 37%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) 8%N None Mk_annot :t: - Smt (DefineConst 38%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 37%Z) Mk_annot) Mk_annot)) Mk_annot :t: - WriteReg "x19" [] (RegVal_Base (Val_Symbolic 38%Z)) Mk_annot :t: + ReadReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: + Smt (DefineConst 19%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DefineConst 25%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DeclareConst 29%Z (Ty_BitVec 64%N)) Mk_annot :t: + ReadMem (RegVal_Base (Val_Symbolic 29%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) 8%N None Mk_annot :t: + Smt (DefineConst 30%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 29%Z) Mk_annot) Mk_annot)) Mk_annot :t: + WriteReg "x19" [] (RegVal_Base (Val_Symbolic 30%Z)) Mk_annot :t: WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t: tnil . diff --git a/instructions/binary_search_riscv64/a88.v b/instructions/binary_search_riscv64/a88.v index 996bd95..8e5f853 100644 --- a/instructions/binary_search_riscv64/a88.v +++ b/instructions/binary_search_riscv64/a88.v @@ -1,7 +1,7 @@ From isla Require Import opsem. Definition a88 : isla_trace := - AssumeReg "rv_enable_pmp" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: + AssumeReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: AssumeReg "rv_enable_misaligned_access" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: AssumeReg "rv_ram_base" [] (RegVal_Base (Val_Bits (BV 64%N 0x80000000%Z))) Mk_annot :t: AssumeReg "rv_ram_size" [] (RegVal_Base (Val_Bits (BV 64%N 0x4000000%Z))) Mk_annot :t: @@ -27,14 +27,13 @@ Definition a88 : isla_trace := Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x20%Z)) Mk_annot] Mk_annot)) Mk_annot :t: ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t: ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t: - Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t: - Smt (DefineConst 27%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DefineConst 33%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DeclareConst 37%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadMem (RegVal_Base (Val_Symbolic 37%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) 8%N None Mk_annot :t: - Smt (DefineConst 38%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 37%Z) Mk_annot) Mk_annot)) Mk_annot :t: - WriteReg "x18" [] (RegVal_Base (Val_Symbolic 38%Z)) Mk_annot :t: + ReadReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: + Smt (DefineConst 19%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DefineConst 25%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DeclareConst 29%Z (Ty_BitVec 64%N)) Mk_annot :t: + ReadMem (RegVal_Base (Val_Symbolic 29%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) 8%N None Mk_annot :t: + Smt (DefineConst 30%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 29%Z) Mk_annot) Mk_annot)) Mk_annot :t: + WriteReg "x18" [] (RegVal_Base (Val_Symbolic 30%Z)) Mk_annot :t: WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t: tnil . diff --git a/instructions/binary_search_riscv64/a8c.v b/instructions/binary_search_riscv64/a8c.v index 5c8e682..65f1e09 100644 --- a/instructions/binary_search_riscv64/a8c.v +++ b/instructions/binary_search_riscv64/a8c.v @@ -1,7 +1,7 @@ From isla Require Import opsem. Definition a8c : isla_trace := - AssumeReg "rv_enable_pmp" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: + AssumeReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: AssumeReg "rv_enable_misaligned_access" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: AssumeReg "rv_ram_base" [] (RegVal_Base (Val_Bits (BV 64%N 0x80000000%Z))) Mk_annot :t: AssumeReg "rv_ram_size" [] (RegVal_Base (Val_Bits (BV 64%N 0x4000000%Z))) Mk_annot :t: @@ -27,14 +27,13 @@ Definition a8c : isla_trace := Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x28%Z)) Mk_annot] Mk_annot)) Mk_annot :t: ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t: ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t: - Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t: - Smt (DefineConst 27%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DefineConst 33%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DeclareConst 37%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadMem (RegVal_Base (Val_Symbolic 37%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) 8%N None Mk_annot :t: - Smt (DefineConst 38%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 37%Z) Mk_annot) Mk_annot)) Mk_annot :t: - WriteReg "x9" [] (RegVal_Base (Val_Symbolic 38%Z)) Mk_annot :t: + ReadReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: + Smt (DefineConst 19%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DefineConst 25%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DeclareConst 29%Z (Ty_BitVec 64%N)) Mk_annot :t: + ReadMem (RegVal_Base (Val_Symbolic 29%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) 8%N None Mk_annot :t: + Smt (DefineConst 30%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 29%Z) Mk_annot) Mk_annot)) Mk_annot :t: + WriteReg "x9" [] (RegVal_Base (Val_Symbolic 30%Z)) Mk_annot :t: WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t: tnil . diff --git a/instructions/binary_search_riscv64/a90.v b/instructions/binary_search_riscv64/a90.v index b3ce29e..2506f0c 100644 --- a/instructions/binary_search_riscv64/a90.v +++ b/instructions/binary_search_riscv64/a90.v @@ -1,7 +1,7 @@ From isla Require Import opsem. Definition a90 : isla_trace := - AssumeReg "rv_enable_pmp" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: + AssumeReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: AssumeReg "rv_enable_misaligned_access" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: AssumeReg "rv_ram_base" [] (RegVal_Base (Val_Bits (BV 64%N 0x80000000%Z))) Mk_annot :t: AssumeReg "rv_ram_size" [] (RegVal_Base (Val_Bits (BV 64%N 0x4000000%Z))) Mk_annot :t: @@ -27,14 +27,13 @@ Definition a90 : isla_trace := Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x30%Z)) Mk_annot] Mk_annot)) Mk_annot :t: ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t: ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t: - Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t: - Smt (DefineConst 27%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DefineConst 33%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DeclareConst 37%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadMem (RegVal_Base (Val_Symbolic 37%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) 8%N None Mk_annot :t: - Smt (DefineConst 38%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 37%Z) Mk_annot) Mk_annot)) Mk_annot :t: - WriteReg "x8" [] (RegVal_Base (Val_Symbolic 38%Z)) Mk_annot :t: + ReadReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: + Smt (DefineConst 19%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DefineConst 25%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DeclareConst 29%Z (Ty_BitVec 64%N)) Mk_annot :t: + ReadMem (RegVal_Base (Val_Symbolic 29%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) 8%N None Mk_annot :t: + Smt (DefineConst 30%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 29%Z) Mk_annot) Mk_annot)) Mk_annot :t: + WriteReg "x8" [] (RegVal_Base (Val_Symbolic 30%Z)) Mk_annot :t: WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t: tnil . diff --git a/instructions/binary_search_riscv64/a94.v b/instructions/binary_search_riscv64/a94.v index 348caa8..b902b54 100644 --- a/instructions/binary_search_riscv64/a94.v +++ b/instructions/binary_search_riscv64/a94.v @@ -1,7 +1,7 @@ From isla Require Import opsem. Definition a94 : isla_trace := - AssumeReg "rv_enable_pmp" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: + AssumeReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: AssumeReg "rv_enable_misaligned_access" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: AssumeReg "rv_ram_base" [] (RegVal_Base (Val_Bits (BV 64%N 0x80000000%Z))) Mk_annot :t: AssumeReg "rv_ram_size" [] (RegVal_Base (Val_Bits (BV 64%N 0x4000000%Z))) Mk_annot :t: @@ -27,14 +27,13 @@ Definition a94 : isla_trace := Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x38%Z)) Mk_annot] Mk_annot)) Mk_annot :t: ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t: ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t: - Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t: - Smt (DefineConst 27%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DefineConst 33%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DeclareConst 37%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadMem (RegVal_Base (Val_Symbolic 37%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) 8%N None Mk_annot :t: - Smt (DefineConst 38%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 37%Z) Mk_annot) Mk_annot)) Mk_annot :t: - WriteReg "x1" [] (RegVal_Base (Val_Symbolic 38%Z)) Mk_annot :t: + ReadReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: + Smt (DefineConst 19%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DefineConst 25%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DeclareConst 29%Z (Ty_BitVec 64%N)) Mk_annot :t: + ReadMem (RegVal_Base (Val_Symbolic 29%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) 8%N None Mk_annot :t: + Smt (DefineConst 30%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 29%Z) Mk_annot) Mk_annot)) Mk_annot :t: + WriteReg "x1" [] (RegVal_Base (Val_Symbolic 30%Z)) Mk_annot :t: WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t: tnil . diff --git a/instructions/binary_search_riscv64/ac.v b/instructions/binary_search_riscv64/ac.v index fa56cee..a9086f4 100644 --- a/instructions/binary_search_riscv64/ac.v +++ b/instructions/binary_search_riscv64/ac.v @@ -1,7 +1,7 @@ From isla Require Import opsem. Definition ac : isla_trace := - AssumeReg "rv_enable_pmp" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: + AssumeReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: AssumeReg "rv_enable_misaligned_access" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: AssumeReg "rv_ram_base" [] (RegVal_Base (Val_Bits (BV 64%N 0x80000000%Z))) Mk_annot :t: AssumeReg "rv_ram_size" [] (RegVal_Base (Val_Bits (BV 64%N 0x4000000%Z))) Mk_annot :t: @@ -27,14 +27,13 @@ Definition ac : isla_trace := Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x28%Z)) Mk_annot] Mk_annot)) Mk_annot :t: ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t: ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t: - Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t: - Smt (DeclareConst 25%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadReg "x9" [] (RegVal_Base (Val_Symbolic 25%Z)) Mk_annot :t: - Smt (DefineConst 28%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DefineConst 34%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DeclareConst 38%Z Ty_Bool) Mk_annot :t: - WriteMem (RegVal_Base (Val_Symbolic 38%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) (RegVal_Base (Val_Symbolic 25%Z)) 8%N None Mk_annot :t: + Smt (DeclareConst 17%Z (Ty_BitVec 64%N)) Mk_annot :t: + ReadReg "x9" [] (RegVal_Base (Val_Symbolic 17%Z)) Mk_annot :t: + ReadReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: + Smt (DefineConst 20%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DefineConst 26%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DeclareConst 30%Z Ty_Bool) Mk_annot :t: + WriteMem (RegVal_Base (Val_Symbolic 30%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) (RegVal_Base (Val_Symbolic 17%Z)) 8%N None Mk_annot :t: WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t: tnil . diff --git a/instructions/memcpy_riscv64/a4.v b/instructions/memcpy_riscv64/a4.v index 1634c13..aaec855 100644 --- a/instructions/memcpy_riscv64/a4.v +++ b/instructions/memcpy_riscv64/a4.v @@ -1,7 +1,7 @@ From isla Require Import opsem. Definition a4 : isla_trace := - AssumeReg "rv_enable_pmp" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: + AssumeReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: AssumeReg "rv_enable_misaligned_access" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: AssumeReg "rv_ram_base" [] (RegVal_Base (Val_Bits (BV 64%N 0x80000000%Z))) Mk_annot :t: AssumeReg "rv_ram_size" [] (RegVal_Base (Val_Bits (BV 64%N 0x4000000%Z))) Mk_annot :t: @@ -26,14 +26,13 @@ Definition a4 : isla_trace := Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t: ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t: ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t: - Smt (DeclareConst 14%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadReg "satp" [] (RegVal_Base (Val_Symbolic 14%Z)) Mk_annot :t: - Smt (DefineConst 21%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DefineConst 27%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DeclareConst 31%Z (Ty_BitVec 8%N)) Mk_annot :t: - ReadMem (RegVal_Base (Val_Symbolic 31%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) 1%N None Mk_annot :t: - Smt (DefineConst 32%Z (Unop (SignExtend 56%N) (Val (Val_Symbolic 31%Z) Mk_annot) Mk_annot)) Mk_annot :t: - WriteReg "x13" [] (RegVal_Base (Val_Symbolic 32%Z)) Mk_annot :t: + ReadReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: + Smt (DefineConst 13%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DefineConst 19%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DeclareConst 23%Z (Ty_BitVec 8%N)) Mk_annot :t: + ReadMem (RegVal_Base (Val_Symbolic 23%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) 1%N None Mk_annot :t: + Smt (DefineConst 24%Z (Unop (SignExtend 56%N) (Val (Val_Symbolic 23%Z) Mk_annot) Mk_annot)) Mk_annot :t: + WriteReg "x13" [] (RegVal_Base (Val_Symbolic 24%Z)) Mk_annot :t: WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t: tnil . diff --git a/instructions/memcpy_riscv64/a8.v b/instructions/memcpy_riscv64/a8.v index fe866c4..bd7e45b 100644 --- a/instructions/memcpy_riscv64/a8.v +++ b/instructions/memcpy_riscv64/a8.v @@ -1,7 +1,7 @@ From isla Require Import opsem. Definition a8 : isla_trace := - AssumeReg "rv_enable_pmp" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: + AssumeReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: AssumeReg "rv_enable_misaligned_access" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: AssumeReg "rv_ram_base" [] (RegVal_Base (Val_Bits (BV 64%N 0x80000000%Z))) Mk_annot :t: AssumeReg "rv_ram_size" [] (RegVal_Base (Val_Bits (BV 64%N 0x4000000%Z))) Mk_annot :t: @@ -26,15 +26,14 @@ Definition a8 : isla_trace := Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x0%Z)) Mk_annot] Mk_annot)) Mk_annot :t: ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t: ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t: - Smt (DeclareConst 14%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadReg "satp" [] (RegVal_Base (Val_Symbolic 14%Z)) Mk_annot :t: - Smt (DeclareConst 19%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadReg "x13" [] (RegVal_Base (Val_Symbolic 19%Z)) Mk_annot :t: - Smt (DefineConst 20%Z (Unop (Extract 7%N 0%N) (Val (Val_Symbolic 19%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DefineConst 23%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DefineConst 29%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DeclareConst 33%Z Ty_Bool) Mk_annot :t: - WriteMem (RegVal_Base (Val_Symbolic 33%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) (RegVal_Base (Val_Symbolic 20%Z)) 1%N None Mk_annot :t: + Smt (DeclareConst 11%Z (Ty_BitVec 64%N)) Mk_annot :t: + ReadReg "x13" [] (RegVal_Base (Val_Symbolic 11%Z)) Mk_annot :t: + Smt (DefineConst 12%Z (Unop (Extract 7%N 0%N) (Val (Val_Symbolic 11%Z) Mk_annot) Mk_annot)) Mk_annot :t: + ReadReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: + Smt (DefineConst 15%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DefineConst 21%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DeclareConst 25%Z Ty_Bool) Mk_annot :t: + WriteMem (RegVal_Base (Val_Symbolic 25%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) (RegVal_Base (Val_Symbolic 12%Z)) 1%N None Mk_annot :t: WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t: tnil . diff --git a/instructions/riscv64_test/a8.v b/instructions/riscv64_test/a8.v index c9101ab..4e1ccb9 100644 --- a/instructions/riscv64_test/a8.v +++ b/instructions/riscv64_test/a8.v @@ -1,7 +1,7 @@ From isla Require Import opsem. Definition a8 : isla_trace := - AssumeReg "rv_enable_pmp" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: + AssumeReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: AssumeReg "rv_enable_misaligned_access" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: AssumeReg "rv_ram_base" [] (RegVal_Base (Val_Bits (BV 64%N 0x80000000%Z))) Mk_annot :t: AssumeReg "rv_ram_size" [] (RegVal_Base (Val_Bits (BV 64%N 0x4000000%Z))) Mk_annot :t: @@ -27,14 +27,13 @@ Definition a8 : isla_trace := Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x8%Z)) Mk_annot] Mk_annot)) Mk_annot :t: ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t: ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t: - Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t: - Smt (DeclareConst 25%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadReg "x11" [] (RegVal_Base (Val_Symbolic 25%Z)) Mk_annot :t: - Smt (DefineConst 28%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DefineConst 34%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DeclareConst 38%Z Ty_Bool) Mk_annot :t: - WriteMem (RegVal_Base (Val_Symbolic 38%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) (RegVal_Base (Val_Symbolic 25%Z)) 8%N None Mk_annot :t: + Smt (DeclareConst 17%Z (Ty_BitVec 64%N)) Mk_annot :t: + ReadReg "x11" [] (RegVal_Base (Val_Symbolic 17%Z)) Mk_annot :t: + ReadReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: + Smt (DefineConst 20%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DefineConst 26%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DeclareConst 30%Z Ty_Bool) Mk_annot :t: + WriteMem (RegVal_Base (Val_Symbolic 30%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) (RegVal_Base (Val_Symbolic 17%Z)) 8%N None Mk_annot :t: WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t: tnil . diff --git a/instructions/riscv64_test/ac.v b/instructions/riscv64_test/ac.v index b1b1d48..c95e7f3 100644 --- a/instructions/riscv64_test/ac.v +++ b/instructions/riscv64_test/ac.v @@ -1,7 +1,7 @@ From isla Require Import opsem. Definition ac : isla_trace := - AssumeReg "rv_enable_pmp" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: + AssumeReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: AssumeReg "rv_enable_misaligned_access" [] (RegVal_Base (Val_Bool false)) Mk_annot :t: AssumeReg "rv_ram_base" [] (RegVal_Base (Val_Bits (BV 64%N 0x80000000%Z))) Mk_annot :t: AssumeReg "rv_ram_size" [] (RegVal_Base (Val_Bits (BV 64%N 0x4000000%Z))) Mk_annot :t: @@ -27,14 +27,13 @@ Definition ac : isla_trace := Smt (DefineConst 6%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 3%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x8%Z)) Mk_annot] Mk_annot)) Mk_annot :t: ReadReg "mstatus" [] (RegVal_Struct [("bits", RegVal_Base (Val_Symbolic 1%Z))]) Mk_annot :t: ReadReg "cur_privilege" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t: - Smt (DeclareConst 20%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadReg "satp" [] (RegVal_Base (Val_Symbolic 20%Z)) Mk_annot :t: - Smt (DefineConst 27%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DefineConst 33%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: - Smt (DeclareConst 37%Z (Ty_BitVec 64%N)) Mk_annot :t: - ReadMem (RegVal_Base (Val_Symbolic 37%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) 8%N None Mk_annot :t: - Smt (DefineConst 38%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 37%Z) Mk_annot) Mk_annot)) Mk_annot :t: - WriteReg "x11" [] (RegVal_Base (Val_Symbolic 38%Z)) Mk_annot :t: + ReadReg "rv_pmp_count" [] (RegVal_I 0%Z 64%Z) Mk_annot :t: + Smt (DefineConst 19%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DefineConst 25%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 6%Z) Mk_annot) Mk_annot)) Mk_annot :t: + Smt (DeclareConst 29%Z (Ty_BitVec 64%N)) Mk_annot :t: + ReadMem (RegVal_Base (Val_Symbolic 29%Z)) (RegVal_Poison) (RegVal_Base (Val_Symbolic 6%Z)) 8%N None Mk_annot :t: + Smt (DefineConst 30%Z (Unop (SignExtend 0%N) (Val (Val_Symbolic 29%Z) Mk_annot) Mk_annot)) Mk_annot :t: + WriteReg "x11" [] (RegVal_Base (Val_Symbolic 30%Z)) Mk_annot :t: WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t: tnil . diff --git a/theories/riscv64/sys_regs.v b/theories/riscv64/sys_regs.v index e5157f8..0c5f5f3 100644 --- a/theories/riscv64/sys_regs.v +++ b/theories/riscv64/sys_regs.v @@ -71,6 +71,7 @@ Definition sys_regs : list (reg_kind * valu_shape) := [ (KindReg "rv_rom_size" , ExactShape (RVal_Bits (BV 64 0x0000000000000100))); (KindReg "rv_clint_base" , ExactShape (RVal_Bits (BV 64 0x0000000002000000))); (KindReg "rv_clint_size" , ExactShape (RVal_Bits (BV 64 0x00000000000c0000))); + (KindReg "rv_pmp_count" , ExactShape (RegVal_I 0 64)); (KindReg "rv_htif_tohost" , ExactShape (RVal_Bits (BV 64 0x0000000040001000))); (KindReg "cur_privilege" , ExactShape (RVal_Enum "Machine")); (* TODO: remove this *) @@ -90,6 +91,7 @@ Definition sys_regs_map (mstatus_bits satp : bv 64) : reg_map := <[ "rv_rom_size" := RVal_Bits (BV 64 0x0000000000000100) ]> $ <[ "rv_clint_base" := RVal_Bits (BV 64 0x0000000002000000) ]> $ <[ "rv_clint_size" := RVal_Bits (BV 64 0x00000000000c0000) ]> $ + <[ "rv_pmp_count" := RegVal_I 0 64 ]> $ <[ "rv_htif_tohost" := RVal_Bits (BV 64 0x0000000040001000) ]> $ <[ "cur_privilege" := RVal_Enum "Machine" ]> $ <[ "Machine" := RVal_Enum "Machine" ]> $