Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adapted islaris to the latest isla and to the (currently under review) latest isla-lang #25

Merged
merged 13 commits into from
Dec 5, 2023
Merged

Adapted islaris to the latest isla and to the (currently under review) latest isla-lang #25

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
4838855
Updated the build instructions for isla-lang: use the latest version now
Aug 29, 2022
72c9614
Merge branch 'main' of https://github.com/rems-project/islaris into r…
ric-almeida Oct 27, 2023
09b9506
Merge branch 'rems-project-main'
ric-almeida Oct 27, 2023
2651aa8
New line
ric-almeida Oct 27, 2023
a3187b8
- Adapted islaris to the new trace syntax for the enumerate types and…
ric-almeida Nov 22, 2023
ca6043c
Merge pull request #2 from rems-project/main
ric-almeida Nov 22, 2023
f46ef5a
Updated isla commit to the latest one
ric-almeida Nov 22, 2023
1f4e38e
Updated isla-lang pin instruction on Makefile to temporary fork
ric-almeida Nov 23, 2023
2b3af6c
Update ci.yml
ric-almeida Nov 23, 2023
28d9880
Update .gitlab-ci.yml
ric-almeida Nov 23, 2023
6dddee2
Set Smt(DefineEnum(_,_,_), _) to true
ric-almeida Dec 4, 2023
5650bd2
Merge branch 'main' of https://github.com/ric-almeida/islaris
ric-almeida Dec 4, 2023
35a58c3
Update pin to isla-lang after the new version was merged into the mai…
ric-almeida Dec 5, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .github/workflows/ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@ jobs:

env:
OCAML: "ocaml-variants.4.14.0+options ocaml-option-flambda"
OPAM_PINS: "coq version 8.17.0 isla-lang git git+https://git@github.com/rems-project/isla-lang.git#4ee3daa3a9f04b2d6a55dd94026ff5f9d79db5fc"
OPAM_PINS: "coq version 8.17.0 isla-lang git git+https://github.com/rems-project/isla-lang.git"
CPU_CORES: "1"
DENY_WARNINGS: "1"
CI_RUNNER: "dummy"
Expand Down
6 changes: 3 additions & 3 deletions .gitlab-ci.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ variables:
build-coq.8.17.0-timing:
<<: *template
variables:
OPAM_PINS: "coq version 8.17.0 isla-lang git git+https://git@github.com/rems-project/isla-lang.git#4ee3daa3a9f04b2d6a55dd94026ff5f9d79db5fc"
OPAM_PINS: "coq version 8.17.0 isla-lang git git+https://github.com/rems-project/isla-lang.git"
DENY_WARNINGS: "1"
# OPAM_PKG: "1"
only:
Expand All @@ -46,15 +46,15 @@ build-coq.8.17.0-timing:
build-coq.8.17.0:
<<: *template
variables:
OPAM_PINS: "coq version 8.17.0 isla-lang git git+https://git@github.com/rems-project/isla-lang.git#4ee3daa3a9f04b2d6a55dd94026ff5f9d79db5fc"
OPAM_PINS: "coq version 8.17.0 isla-lang git git+https://github.com/rems-project/isla-lang.git"
DENY_WARNINGS: "1"
only:
- /^ci/@iris/isla-coq

trigger-iris.dev:
<<: *template
variables:
OPAM_PINS: "coq version 8.17.0 coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV isla-lang git git+https://git@github.com/rems-project/isla-lang.git#4ee3daa3a9f04b2d6a55dd94026ff5f9d79db5fc"
OPAM_PINS: "coq version 8.17.0 coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV isla-lang git git+https://github.com/rems-project/isla-lang.git"
except:
only:
- triggers
Expand Down
2 changes: 1 addition & 1 deletion Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -102,7 +102,7 @@ strip_license:

# We cannot use builddep-pins as a dependency of builddep-opamfiles because the CI removes all pins.
builddep-pins:
@opam pin add -n -y isla-lang "git+https://git@github.com/rems-project/isla-lang.git#4ee3daa3a9f04b2d6a55dd94026ff5f9d79db5fc"
@opam pin add -n -y isla-lang "git+https://github.com/rems-project/isla-lang.git"
.PHONY: builddep-pins

builddep-opamfiles: builddep/islaris-builddep.opam
Expand Down
2 changes: 1 addition & 1 deletion README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ to point to a working checkout of Isla resp. Isla snapshots.)

The following commits of isla and isla-snapshots are tested:
```
isla: 473f9986832d95b6c4ebb192bb075f2095a92df1
isla: b8e614bda4a20e42c37d8b216853653133d04322
isla-snapshots: b58da9170470a422c9396983ac8f87f0a63ba6f8
```

Expand Down
13 changes: 2 additions & 11 deletions deps/Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,22 +1,13 @@
SAIL_COMMIT=605cd3cffe4b18fb5d0a99beef5d6ee33e1a7dcb
BBV_COMMIT=6144e214583b72182a4ed89e4328ea62ba766e2e

all: sail-riscv-coq
.PHONY: all

sail-%.tar.gz:
wget "https://github.com/rems-project/sail/archive/$*.tar.gz" -O $@

bbv-%.tar.gz:
wget "https://github.com/mit-plv/bbv/archive/$*.tar.gz" -O $@

# TODO: maybe add opam install z3?
bbv: bbv-$(BBV_COMMIT).tar.gz
rm -rf coq-bbv
tar xf bbv-$(BBV_COMMIT).tar.gz
mv "bbv-${BBV_COMMIT}" coq-bbv
cp coq-bbv-1.3.opam coq-bbv/opam
opam pin add ./coq-bbv -n
bbv:
opam pin --yes coq-bbv 1.4
.PHONY: bbv

# TODO: maybe add opam install z3?
Expand Down
1 change: 1 addition & 0 deletions etc/aarch64_isla_coq.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ write_exclusives = ["Write_exclusive", "Write_exclusive_release"]
assembler = "aarch64-linux-gnu-as -march=armv8.1-a"
objdump = "aarch64-linux-gnu-objdump"
linker = "aarch64-linux-gnu-ld"
nm = "aarch64-linux-gnu-nm"

[mmu]
page_table_base = "0x300000"
Expand Down
1 change: 1 addition & 0 deletions etc/aarch64_isla_coq_el1.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ write_exclusives = ["Write_exclusive", "Write_exclusive_release"]
assembler = "aarch64-linux-gnu-as -march=armv8.1-a"
objdump = "aarch64-linux-gnu-objdump"
linker = "aarch64-linux-gnu-ld"
nm = "aarch64-linux-gnu-nm"

[mmu]
page_table_base = "0x300000"
Expand Down
1 change: 1 addition & 0 deletions etc/aarch64_isla_coq_pkvm.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ write_exclusives = ["Write_exclusive", "Write_exclusive_release"]
assembler = "aarch64-linux-gnu-as -march=armv8.1-a"
objdump = "aarch64-linux-gnu-objdump"
linker = "aarch64-linux-gnu-ld"
nm = "aarch64-linux-gnu-nm"

[mmu]
page_table_base = "0x300000"
Expand Down
4 changes: 4 additions & 0 deletions etc/riscv64_isla_coq.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,10 @@ write_exclusives = ["Write_RISCV_conditional", "Write_RISCV_conditional_release"
assembler = "riscv64-linux-gnu-as -march=rv64imac"
objdump = "riscv64-linux-gnu-objdump"
linker = "riscv64-linux-gnu-ld"
nm = "riscv64-linux-gnu-nm"

[const_primops]
platform_write_mem_ea = false

# Currently not used for RISC-V
[mmu]
Expand Down
38 changes: 20 additions & 18 deletions frontend/coq_pp.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,7 +88,7 @@ let pp_lrng ff _ =
let pp_var_name ff i =
Format.fprintf ff "%a" pp_Z i

let pp_register_name ff r =
let pp_sail_name ff r =
Format.fprintf ff "%S" r

let remove_zeroes digits =
Expand Down Expand Up @@ -127,13 +127,13 @@ let pp_bv ff s =
let pp_accessor ff a =
let pp fmt = Format.fprintf ff fmt in
match a with
| Ast.Field(r) -> pp "Field %a" pp_register_name r
| Ast.Field(r) -> pp "Field %a" pp_sail_name r

let pp_accessor_list ff l =
pp_list pp_accessor ff (match l with Ast.Nil -> [] | Ast.Cons(l) -> l)

let pp_enum_id ff i =
Format.fprintf ff "(Mk_enum_id %i%%nat)" i
Format.fprintf ff "\"%s\"" i

let rec pp_ty ff ty =
let pp fmt = Format.fprintf ff fmt in
Expand Down Expand Up @@ -214,11 +214,11 @@ let pp_manyop ff o =
| Ast.Concat -> pp "Concat"

let pp_enum_ctor ff n =
Format.fprintf ff "Mk_enum_ctor %i%%nat" n
Format.fprintf ff "\"%s\"" n

let pp_enum ff e =
let pp fmt = Format.fprintf ff fmt in
pp "(%a, %a)" pp_enum_id (fst e) pp_enum_ctor (snd e)
pp "%a" pp_enum_ctor e

let pp_base_val ff v =
let pp fmt = Format.fprintf ff fmt in
Expand All @@ -236,7 +236,7 @@ let pp_assume_val ff v =
let pp fmt = Format.fprintf ff fmt in
match v with
| Ast.AVal_Var(r,l) ->
pp "AVal_Var %a %a" pp_register_name r pp_accessor_list l
pp "AVal_Var %a %a" pp_sail_name r pp_accessor_list l
| Ast.AVal_Bool(b) ->
pp "AVal_Bool %b" b
| Ast.AVal_Bits(s) ->
Expand All @@ -261,11 +261,11 @@ let rec pp_valu ff v =
pp "RegVal_List %a" (pp_list pp_valu) l
| Ast.RegVal_Struct(l) ->
let pp_elt ff (r, v) =
Format.fprintf ff "(%a, %a)" pp_register_name r pp_valu v
Format.fprintf ff "(%a, %a)" pp_sail_name r pp_valu v
in
pp "RegVal_Struct %a" (pp_list pp_elt) l
| Ast.RegVal_Constructor(r, v) ->
pp "RegVal_Constructor %a (%a)" pp_register_name r pp_valu v
pp "RegVal_Constructor %a (%a)" pp_sail_name r pp_valu v
| Ast.RegVal_Poison ->
pp "RegVal_Poison"

Expand Down Expand Up @@ -311,8 +311,8 @@ let pp_smt ff e =
pp "DefineConst %a (%a)" pp_var_name i pp_exp e
| Ast.Assert(e) ->
pp "Assert (%a)" pp_exp e
| Ast.DefineEnum(i) ->
pp "DefineEnum %a" pp_Z i
| Ast.DefineEnum(name,len,l) ->
pp "DefineEnum %a %a %a" pp_sail_name name pp_Z len (pp_list pp_sail_name) l

let pp_event ff e =
let pp fmt = Format.fprintf ff fmt in
Expand All @@ -322,10 +322,10 @@ let pp_event ff e =
| Ast.Branch(i,s,a) ->
pp "Branch %a %a %a" pp_Z i pp_str s pp_lrng a
| Ast.ReadReg(r,l,v,a) ->
pp "ReadReg %a %a (%a) %a" pp_register_name r pp_accessor_list l
pp "ReadReg %a %a (%a) %a" pp_sail_name r pp_accessor_list l
pp_valu v pp_lrng a
| Ast.WriteReg(r,l,v,a) ->
pp "WriteReg %a %a (%a) %a" pp_register_name r pp_accessor_list l
pp "WriteReg %a %a (%a) %a" pp_sail_name r pp_accessor_list l
pp_valu v pp_lrng a
| Ast.ReadMem(v1,v2,v3,i,v,a) ->
(* TODO: We remove the kind information since it is quite big and not used.
Expand Down Expand Up @@ -362,18 +362,20 @@ let pp_event ff e =
| Ast.SleepRequest(a) ->
pp "SleepRequest %a" pp_lrng a
| Ast.AssumeReg(r,l,v,a) ->
pp "AssumeReg %a %a (%a) %a" pp_register_name r pp_accessor_list l
pp "AssumeReg %a %a (%a) %a" pp_sail_name r pp_accessor_list l
pp_valu v pp_lrng a
| Ast.Assume(e,a) ->
pp "Assume (%a) %a" pp_a_exp e pp_lrng a
| Ast.FunAssume(r,v,args,a) ->
pp "FunAssume %a %a %a %a" pp_register_name r pp_valu v pp_arg_list args pp_lrng a
pp "FunAssume %a %a %a %a" pp_sail_name r pp_valu v pp_arg_list args pp_lrng a
| Ast.UseFunAssume(r,v,args,a) ->
pp "UseFunAssume %a %a %a %a" pp_register_name r pp_valu v pp_arg_list args pp_lrng a
pp "UseFunAssume %a %a %a %a" pp_sail_name r pp_valu v pp_arg_list args pp_lrng a
| Ast.AbstractCall(r,v,args,a) ->
pp "AbstractCall %a %a %a %a" pp_register_name r pp_valu v pp_arg_list args pp_lrng a
| Ast.AbstractPrimop(r,v,args,a) ->
pp "AbstractPrimop %a %a %a %a" pp_register_name r pp_valu v pp_arg_list args pp_lrng a
pp "AbstractCall %a %a %a %a" pp_sail_name r pp_valu v pp_arg_list args pp_lrng a
| Ast.AbstractPrimop(r,v,args,a) ->
pp "AbstractPrimop %a %a %a %a" pp_sail_name r pp_valu v pp_arg_list args pp_lrng a
| Call (_, _) -> () (* TODO: fill in here? *)
| Return (_, _) -> () (* TODO: fill in here? *)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Probably we should output the Coq constructors for these and filter them somewhere else if we don't want them, but it's not very important.


(** [pp_trace_def name] is a pretty-printer for the Coq definition of a trace,
with given definition name [name]. *)
Expand Down
2 changes: 1 addition & 1 deletion frontend/decomp.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,7 @@ let event_filter : Arch.t -> int -> event -> bool = fun arch i e ->
| Smt(Assert(_), _) -> i = 0
| Cycle(_)
| MarkReg(_, _, _)
| Smt(DefineEnum(_), _) -> false
| Smt(DefineEnum(_,_,_), _) -> true
| _ -> true

(** [gen_coq arch name isla_f coq_f] processes Isla file [isla_f] and produces
Expand Down
8 changes: 4 additions & 4 deletions instructions/binary_search_riscv64/a0.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,10 +4,10 @@ Definition a0 : isla_trace :=
Smt (DeclareConst 0%Z (Ty_BitVec 64%N)) Mk_annot :t:
ReadReg "PC" [] (RegVal_Base (Val_Symbolic 0%Z)) Mk_annot :t:
Smt (DefineConst 1%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 0%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
Smt (DeclareConst 13%Z (Ty_BitVec 64%N)) Mk_annot :t:
ReadReg "x2" [] (RegVal_Base (Val_Symbolic 13%Z)) Mk_annot :t:
Smt (DefineConst 14%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 13%Z) Mk_annot; Val (Val_Bits (BV 64%N 0xffffffffffffffc0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
WriteReg "x2" [] (RegVal_Base (Val_Symbolic 14%Z)) Mk_annot :t:
Smt (DeclareConst 2%Z (Ty_BitVec 64%N)) Mk_annot :t:
ReadReg "x2" [] (RegVal_Base (Val_Symbolic 2%Z)) Mk_annot :t:
Smt (DefineConst 3%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 2%Z) Mk_annot; Val (Val_Bits (BV 64%N 0xffffffffffffffc0%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
WriteReg "x2" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
WriteReg "PC" [] (RegVal_Base (Val_Symbolic 1%Z)) Mk_annot :t:
tnil
.
34 changes: 17 additions & 17 deletions instructions/binary_search_riscv64/a10.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,27 +14,27 @@ Definition a10 : isla_trace :=
Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 2%N) (AExp_Val (AVal_Var "misa" [Field "bits"]) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot :t:
Smt (DeclareConst 1%Z (Ty_BitVec 64%N)) Mk_annot :t:
Assume (AExp_Binop (Eq) (AExp_Manyop (Bvmanyarith Bvand) [AExp_Val (AVal_Var "mstatus" [Field "bits"]) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x20000%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
Smt (DeclareConst 6%Z (Ty_Enum (Mk_enum_id 3%nat))) Mk_annot :t:
Smt (DeclareConst 2%Z (Ty_Enum "Privilege")) Mk_annot :t:
Assume (AExp_Binop (Eq) (AExp_Val (AVal_Var "cur_privilege" []) Mk_annot) (AExp_Val (AVal_Var "Machine" []) Mk_annot) Mk_annot) Mk_annot :t:
Smt (DeclareConst 7%Z (Ty_BitVec 64%N)) Mk_annot :t:
Smt (DeclareConst 3%Z (Ty_BitVec 64%N)) Mk_annot :t:
Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 0%N) (AExp_Val (AVal_Var "x2" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 3%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
Assume (AExp_Binop ((Bvcomp Bvuge)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x20%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot) Mk_annot) Mk_annot :t:
Assume (AExp_Binop ((Bvcomp Bvult)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x20%Z)) Mk_annot] Mk_annot) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot; AExp_Val (AVal_Var "rv_ram_size" []) Mk_annot] Mk_annot) Mk_annot) Mk_annot :t:
Smt (DeclareConst 8%Z (Ty_BitVec 64%N)) Mk_annot :t:
ReadReg "PC" [] (RegVal_Base (Val_Symbolic 8%Z)) Mk_annot :t:
Smt (DefineConst 9%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 8%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
ReadReg "x2" [] (RegVal_Base (Val_Symbolic 7%Z)) Mk_annot :t:
Smt (DefineConst 21%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 7%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x20%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
Smt (DeclareConst 4%Z (Ty_BitVec 64%N)) Mk_annot :t:
ReadReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
Smt (DefineConst 5%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 4%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
ReadReg "x2" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
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 6%Z)) Mk_annot :t:
Smt (DeclareConst 35%Z (Ty_BitVec 64%N)) Mk_annot :t:
ReadReg "satp" [] (RegVal_Base (Val_Symbolic 35%Z)) Mk_annot :t:
Smt (DeclareConst 53%Z (Ty_BitVec 64%N)) Mk_annot :t:
ReadReg "x18" [] (RegVal_Base (Val_Symbolic 53%Z)) Mk_annot :t:
Smt (DefineConst 61%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 21%Z) Mk_annot) Mk_annot)) Mk_annot :t:
Smt (DefineConst 67%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 21%Z) Mk_annot) Mk_annot)) Mk_annot :t:
Smt (DeclareConst 71%Z Ty_Bool) Mk_annot :t:
WriteMem (RegVal_Base (Val_Symbolic 71%Z)) (RegVal_Base (Val_Enum ((Mk_enum_id 2%nat), Mk_enum_ctor 0%nat))) (RegVal_Base (Val_Symbolic 21%Z)) (RegVal_Base (Val_Symbolic 53%Z)) 8%N None Mk_annot :t:
WriteReg "PC" [] (RegVal_Base (Val_Symbolic 9%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:
WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t:
tnil
.
4 changes: 2 additions & 2 deletions instructions/binary_search_riscv64/a10_spec.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ Require Import isla.riscv64.riscv64.
Require Export isla.instructions.binary_search_riscv64.a10.

Lemma a10_spec `{!islaG Σ} `{!threadG} pc:
instr pc (Some a10) ⊢
instr_body pc (sd_spec pc "x18" "x2" (32)).
instr pc (Some a10)
⊢ instr_body pc (sd_spec pc "x18" "x2" (32)).
Proof.
iStartProof.
repeat liAStep; liShow.
Expand Down
34 changes: 17 additions & 17 deletions instructions/binary_search_riscv64/a14.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,27 +14,27 @@ Definition a14 : isla_trace :=
Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 2%N) (AExp_Val (AVal_Var "misa" [Field "bits"]) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x1%Z)) Mk_annot) Mk_annot) Mk_annot :t:
Smt (DeclareConst 1%Z (Ty_BitVec 64%N)) Mk_annot :t:
Assume (AExp_Binop (Eq) (AExp_Manyop (Bvmanyarith Bvand) [AExp_Val (AVal_Var "mstatus" [Field "bits"]) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x20000%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Bits (BV 64%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
Smt (DeclareConst 6%Z (Ty_Enum (Mk_enum_id 3%nat))) Mk_annot :t:
Smt (DeclareConst 2%Z (Ty_Enum "Privilege")) Mk_annot :t:
Assume (AExp_Binop (Eq) (AExp_Val (AVal_Var "cur_privilege" []) Mk_annot) (AExp_Val (AVal_Var "Machine" []) Mk_annot) Mk_annot) Mk_annot :t:
Smt (DeclareConst 7%Z (Ty_BitVec 64%N)) Mk_annot :t:
Smt (DeclareConst 3%Z (Ty_BitVec 64%N)) Mk_annot :t:
Assume (AExp_Binop (Eq) (AExp_Unop (Extract 2%N 0%N) (AExp_Val (AVal_Var "x2" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 3%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t:
Assume (AExp_Binop ((Bvcomp Bvuge)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x18%Z)) Mk_annot] Mk_annot) (AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot) Mk_annot) Mk_annot :t:
Assume (AExp_Binop ((Bvcomp Bvult)) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "x2" []) Mk_annot; AExp_Val (AVal_Bits (BV 64%N 0x18%Z)) Mk_annot] Mk_annot) (AExp_Manyop (Bvmanyarith Bvadd) [AExp_Val (AVal_Var "rv_ram_base" []) Mk_annot; AExp_Val (AVal_Var "rv_ram_size" []) Mk_annot] Mk_annot) Mk_annot) Mk_annot :t:
Smt (DeclareConst 8%Z (Ty_BitVec 64%N)) Mk_annot :t:
ReadReg "PC" [] (RegVal_Base (Val_Symbolic 8%Z)) Mk_annot :t:
Smt (DefineConst 9%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 8%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
ReadReg "x2" [] (RegVal_Base (Val_Symbolic 7%Z)) Mk_annot :t:
Smt (DefineConst 21%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 7%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x18%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
Smt (DeclareConst 4%Z (Ty_BitVec 64%N)) Mk_annot :t:
ReadReg "PC" [] (RegVal_Base (Val_Symbolic 4%Z)) Mk_annot :t:
Smt (DefineConst 5%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 4%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t:
ReadReg "x2" [] (RegVal_Base (Val_Symbolic 3%Z)) Mk_annot :t:
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 6%Z)) Mk_annot :t:
Smt (DeclareConst 35%Z (Ty_BitVec 64%N)) Mk_annot :t:
ReadReg "satp" [] (RegVal_Base (Val_Symbolic 35%Z)) Mk_annot :t:
Smt (DeclareConst 53%Z (Ty_BitVec 64%N)) Mk_annot :t:
ReadReg "x19" [] (RegVal_Base (Val_Symbolic 53%Z)) Mk_annot :t:
Smt (DefineConst 61%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 21%Z) Mk_annot) Mk_annot)) Mk_annot :t:
Smt (DefineConst 67%Z (Unop (ZeroExtend 64%N) (Val (Val_Symbolic 21%Z) Mk_annot) Mk_annot)) Mk_annot :t:
Smt (DeclareConst 71%Z Ty_Bool) Mk_annot :t:
WriteMem (RegVal_Base (Val_Symbolic 71%Z)) (RegVal_Base (Val_Enum ((Mk_enum_id 2%nat), Mk_enum_ctor 0%nat))) (RegVal_Base (Val_Symbolic 21%Z)) (RegVal_Base (Val_Symbolic 53%Z)) 8%N None Mk_annot :t:
WriteReg "PC" [] (RegVal_Base (Val_Symbolic 9%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:
WriteReg "PC" [] (RegVal_Base (Val_Symbolic 5%Z)) Mk_annot :t:
tnil
.
4 changes: 2 additions & 2 deletions instructions/binary_search_riscv64/a14_spec.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ Require Import isla.riscv64.riscv64.
Require Export isla.instructions.binary_search_riscv64.a14.

Lemma a14_spec `{!islaG Σ} `{!threadG} pc:
instr pc (Some a14) ⊢
instr_body pc (sd_spec pc "x19" "x2" (24)).
instr pc (Some a14)
⊢ instr_body pc (sd_spec pc "x19" "x2" (24)).
Proof.
iStartProof.
repeat liAStep; liShow.
Expand Down
Loading
Loading