Skip to content

Commit

Permalink
Changes from updating the RISC-V model
Browse files Browse the repository at this point in the history
  • Loading branch information
@bacam
bacam committed Apr 19, 2024
1 parent 271dadb commit 3dafdd0
Show file tree
Hide file tree
Showing 20 changed files with 155 additions and 172 deletions.
17 changes: 8 additions & 9 deletions instructions/binary_search_riscv64/a10.v
View file
Original file line number Diff line number Diff line change
@@ -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:
Expand All @@ -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
.
17 changes: 8 additions & 9 deletions instructions/binary_search_riscv64/a14.v
View file
Original file line number Diff line number Diff line change
@@ -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:
Expand All @@ -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
.
17 changes: 8 additions & 9 deletions instructions/binary_search_riscv64/a18.v
View file
Original file line number Diff line number Diff line change
@@ -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:
Expand All @@ -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
.
17 changes: 8 additions & 9 deletions instructions/binary_search_riscv64/a1c.v
View file
Original file line number Diff line number Diff line change
@@ -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:
Expand All @@ -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
.
17 changes: 8 additions & 9 deletions instructions/binary_search_riscv64/a4.v
View file
Original file line number Diff line number Diff line change
@@ -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:
Expand All @@ -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
.
17 changes: 8 additions & 9 deletions instructions/binary_search_riscv64/a58.v
View file
Original file line number Diff line number Diff line change
@@ -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:
Expand All @@ -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
.
17 changes: 8 additions & 9 deletions instructions/binary_search_riscv64/a7c.v
View file
Original file line number Diff line number Diff line change
@@ -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:
Expand All @@ -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
.
17 changes: 8 additions & 9 deletions instructions/binary_search_riscv64/a8.v
View file
Original file line number Diff line number Diff line change
@@ -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:
Expand All @@ -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
.
17 changes: 8 additions & 9 deletions instructions/binary_search_riscv64/a80.v
View file
Original file line number Diff line number Diff line change
@@ -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:
Expand All @@ -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
.
Loading

0 comments on commit 3dafdd0

Please sign in to comment.