diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 66d14b7..66cac97 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -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://github.com/rems-project/isla-lang.git" + OPAM_PINS: "coq version 8.17.0 isla-lang git git+https://github.com/rems-project/isla-lang.git#309be26729b511570e2d31f69c6ba1ce1dc00779" DENY_WARNINGS: "1" # OPAM_PKG: "1" only: @@ -46,7 +46,7 @@ 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://github.com/rems-project/isla-lang.git" + OPAM_PINS: "coq version 8.17.0 isla-lang git git+https://github.com/rems-project/isla-lang.git#309be26729b511570e2d31f69c6ba1ce1dc00779" DENY_WARNINGS: "1" only: - /^ci/@iris/isla-coq @@ -54,7 +54,7 @@ build-coq.8.17.0: 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://github.com/rems-project/isla-lang.git" + 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#309be26729b511570e2d31f69c6ba1ce1dc00779" except: only: - triggers diff --git a/Makefile b/Makefile index ebc20c9..623f98a 100644 --- a/Makefile +++ b/Makefile @@ -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://github.com/rems-project/isla-lang.git" + @opam pin add -n -y isla-lang "git+https://github.com/rems-project/isla-lang.git#309be26729b511570e2d31f69c6ba1ce1dc00779" .PHONY: builddep-pins builddep-opamfiles: builddep/islaris-builddep.opam diff --git a/deps/Makefile b/deps/Makefile index f64a580..b4176cb 100644 --- a/deps/Makefile +++ b/deps/Makefile @@ -6,10 +6,6 @@ all: sail-riscv-coq sail-%.tar.gz: wget "https://github.com/rems-project/sail/archive/$*.tar.gz" -O $@ -bbv: - opam pin --yes coq-bbv 1.4 -.PHONY: bbv - # TODO: maybe add opam install z3? sail: sail-$(SAIL_COMMIT).tar.gz rm -rf sail @@ -20,7 +16,7 @@ sail: sail-$(SAIL_COMMIT).tar.gz opam pin add coq-sail ./sail/lib/coq -n .PHONY: sail -sail-riscv-coq: bbv sail +sail-riscv-coq: sail opam pin add coq-sail-riscv 'git+https://github.com/riscv/sail-riscv#17a9929821470e119a6d5b4359d0a51d6dae6679' -n opam install coq-sail-riscv .PHONY: sail-riscv-coq diff --git a/frontend/decomp.ml b/frontend/decomp.ml index bef7899..422618d 100644 --- a/frontend/decomp.ml +++ b/frontend/decomp.ml @@ -84,7 +84,7 @@ let event_filter : Arch.t -> int -> event -> bool = fun arch i e -> | Smt(Assert(_), _) -> i = 0 | Cycle(_) | MarkReg(_, _, _) - | Smt(DefineEnum(_,_,_), _) -> true + | Smt(DefineEnum(_,_,_), _) -> false | _ -> true (** [gen_coq arch name isla_f coq_f] processes Isla file [isla_f] and produces diff --git a/instructions/el2_to_el1/a80008.v b/instructions/el2_to_el1/a80008.v index 1d7a05b..e6b7c1f 100644 --- a/instructions/el2_to_el1/a80008.v +++ b/instructions/el2_to_el1/a80008.v @@ -23,7 +23,7 @@ Definition a80008 : isla_trace := Assume (AExp_Binop (Eq) (AExp_Unop (Extract 55%N 55%N) (AExp_Val (AVal_Var "ELR_EL2" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t: ReadReg "ELR_EL2" [] (RegVal_Base (Val_Symbolic 27%Z)) Mk_annot :t: Smt (DefineConst 30%Z (Unop (Extract 55%N 0%N) (Val (Val_Symbolic 27%Z) Mk_annot) Mk_annot)) Mk_annot :t: - AbstractPrimop "sail_eret" RegVal_Unit [RegVal_Base (Val_Symbolic 30%Z)] Mk_annot :t: + AbstractPrimop "sail_eret" (RegVal_Unit) [RegVal_Base (Val_Symbolic 30%Z)] Mk_annot :t: ReadReg "SPSR_EL2" [] (RegVal_Base (Val_Symbolic 26%Z)) Mk_annot :t: WriteReg "PSTATE" [Field "SS"] (RegVal_Struct [("SS", RegVal_Base (Val_Bits (BV 1%N 0x0%Z)))]) Mk_annot :t: Smt (DefineConst 50%Z (Unop (Extract 3%N 2%N) (Val (Val_Symbolic 26%Z) Mk_annot) Mk_annot)) Mk_annot :t: diff --git a/instructions/simple_hvc/a80020.v b/instructions/simple_hvc/a80020.v index e319b10..7774401 100644 --- a/instructions/simple_hvc/a80020.v +++ b/instructions/simple_hvc/a80020.v @@ -23,7 +23,7 @@ Definition a80020 : isla_trace := Assume (AExp_Binop (Eq) (AExp_Unop (Extract 55%N 55%N) (AExp_Val (AVal_Var "ELR_EL2" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t: ReadReg "ELR_EL2" [] (RegVal_Base (Val_Symbolic 27%Z)) Mk_annot :t: Smt (DefineConst 30%Z (Unop (Extract 55%N 0%N) (Val (Val_Symbolic 27%Z) Mk_annot) Mk_annot)) Mk_annot :t: - AbstractPrimop "sail_eret" RegVal_Unit [RegVal_Base (Val_Symbolic 30%Z)] Mk_annot :t: + AbstractPrimop "sail_eret" (RegVal_Unit) [RegVal_Base (Val_Symbolic 30%Z)] Mk_annot :t: ReadReg "SPSR_EL2" [] (RegVal_Base (Val_Symbolic 26%Z)) Mk_annot :t: WriteReg "PSTATE" [Field "SS"] (RegVal_Struct [("SS", RegVal_Base (Val_Bits (BV 1%N 0x0%Z)))]) Mk_annot :t: Smt (DefineConst 50%Z (Unop (Extract 3%N 2%N) (Val (Val_Symbolic 26%Z) Mk_annot) Mk_annot)) Mk_annot :t: diff --git a/instructions/simple_hvc/aa0404.v b/instructions/simple_hvc/aa0404.v index 8655ca0..1ed9474 100644 --- a/instructions/simple_hvc/aa0404.v +++ b/instructions/simple_hvc/aa0404.v @@ -23,7 +23,7 @@ Definition aa0404 : isla_trace := Assume (AExp_Binop (Eq) (AExp_Unop (Extract 55%N 55%N) (AExp_Val (AVal_Var "ELR_EL2" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t: ReadReg "ELR_EL2" [] (RegVal_Base (Val_Symbolic 27%Z)) Mk_annot :t: Smt (DefineConst 30%Z (Unop (Extract 55%N 0%N) (Val (Val_Symbolic 27%Z) Mk_annot) Mk_annot)) Mk_annot :t: - AbstractPrimop "sail_eret" RegVal_Unit [RegVal_Base (Val_Symbolic 30%Z)] Mk_annot :t: + AbstractPrimop "sail_eret" (RegVal_Unit) [RegVal_Base (Val_Symbolic 30%Z)] Mk_annot :t: ReadReg "SPSR_EL2" [] (RegVal_Base (Val_Symbolic 26%Z)) Mk_annot :t: WriteReg "PSTATE" [Field "SS"] (RegVal_Struct [("SS", RegVal_Base (Val_Bits (BV 1%N 0x0%Z)))]) Mk_annot :t: Smt (DefineConst 50%Z (Unop (Extract 3%N 2%N) (Val (Val_Symbolic 26%Z) Mk_annot) Mk_annot)) Mk_annot :t: diff --git a/pkvm_handler/a18258.v b/pkvm_handler/a18258.v index 43e9d25..d78db30 100644 --- a/pkvm_handler/a18258.v +++ b/pkvm_handler/a18258.v @@ -1,7 +1,7 @@ From isla Require Import opsem. Definition a18258 : isla_trace := - AbstractPrimop "sail_barrier" RegVal_Unit [RegVal_Constructor "Barrier_ISB" (RegVal_Unit)] Mk_annot :t: + AbstractPrimop "sail_barrier" (RegVal_Unit) [RegVal_Constructor "Barrier_ISB" (RegVal_Unit)] Mk_annot :t: Smt (DeclareConst 46%Z (Ty_BitVec 64%N)) Mk_annot :t: ReadReg "_PC" [] (RegVal_Base (Val_Symbolic 46%Z)) Mk_annot :t: Smt (DefineConst 47%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 46%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t: diff --git a/pkvm_handler/a18260.v b/pkvm_handler/a18260.v index b3f3f52..4c32376 100644 --- a/pkvm_handler/a18260.v +++ b/pkvm_handler/a18260.v @@ -1,7 +1,7 @@ From isla Require Import opsem. Definition a18260 : isla_trace := - AbstractPrimop "sail_barrier" RegVal_Unit [RegVal_Constructor "Barrier_ISB" (RegVal_Unit)] Mk_annot :t: + AbstractPrimop "sail_barrier" (RegVal_Unit) [RegVal_Constructor "Barrier_ISB" (RegVal_Unit)] Mk_annot :t: Smt (DeclareConst 46%Z (Ty_BitVec 64%N)) Mk_annot :t: ReadReg "_PC" [] (RegVal_Base (Val_Symbolic 46%Z)) Mk_annot :t: Smt (DefineConst 47%Z (Manyop (Bvmanyarith Bvadd) [Val (Val_Symbolic 46%Z) Mk_annot; Val (Val_Bits (BV 64%N 0x4%Z)) Mk_annot] Mk_annot)) Mk_annot :t: diff --git a/pkvm_handler/a18284.v b/pkvm_handler/a18284.v index 18087ef..d079575 100644 --- a/pkvm_handler/a18284.v +++ b/pkvm_handler/a18284.v @@ -24,7 +24,7 @@ Definition a18284 : isla_trace := Assume (AExp_Binop (Eq) (AExp_Unop (Extract 55%N 55%N) (AExp_Val (AVal_Var "ELR_EL2" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t: ReadReg "ELR_EL2" [] (RegVal_Base (Val_Symbolic 27%Z)) Mk_annot :t: Smt (DefineConst 30%Z (Unop (Extract 55%N 0%N) (Val (Val_Symbolic 27%Z) Mk_annot) Mk_annot)) Mk_annot :t: - AbstractPrimop "sail_eret" RegVal_Unit [RegVal_Base (Val_Symbolic 30%Z)] Mk_annot :t: + AbstractPrimop "sail_eret" (RegVal_Unit) [RegVal_Base (Val_Symbolic 30%Z)] Mk_annot :t: ReadReg "SPSR_EL2" [] (RegVal_Base (Val_Symbolic 26%Z)) Mk_annot :t: WriteReg "PSTATE" [Field "SS"] (RegVal_Struct [("SS", RegVal_Base (Val_Bits (BV 1%N 0x0%Z)))]) Mk_annot :t: Smt (DefineConst 50%Z (Unop (Extract 3%N 2%N) (Val (Val_Symbolic 26%Z) Mk_annot) Mk_annot)) Mk_annot :t: diff --git a/pkvm_handler/a18290.v b/pkvm_handler/a18290.v index d9ee7bd..1d13cc7 100644 --- a/pkvm_handler/a18290.v +++ b/pkvm_handler/a18290.v @@ -24,7 +24,7 @@ Definition a18290 : isla_trace := Assume (AExp_Binop (Eq) (AExp_Unop (Extract 55%N 55%N) (AExp_Val (AVal_Var "ELR_EL2" []) Mk_annot) Mk_annot) (AExp_Val (AVal_Bits (BV 1%N 0x0%Z)) Mk_annot) Mk_annot) Mk_annot :t: ReadReg "ELR_EL2" [] (RegVal_Base (Val_Symbolic 27%Z)) Mk_annot :t: Smt (DefineConst 30%Z (Unop (Extract 55%N 0%N) (Val (Val_Symbolic 27%Z) Mk_annot) Mk_annot)) Mk_annot :t: - AbstractPrimop "sail_eret" RegVal_Unit [RegVal_Base (Val_Symbolic 30%Z)] Mk_annot :t: + AbstractPrimop "sail_eret" (RegVal_Unit) [RegVal_Base (Val_Symbolic 30%Z)] Mk_annot :t: ReadReg "SPSR_EL2" [] (RegVal_Base (Val_Symbolic 26%Z)) Mk_annot :t: WriteReg "PSTATE" [Field "SS"] (RegVal_Struct [("SS", RegVal_Base (Val_Bits (BV 1%N 0x0%Z)))]) Mk_annot :t: Smt (DefineConst 50%Z (Unop (Extract 3%N 2%N) (Val (Val_Symbolic 26%Z) Mk_annot) Mk_annot)) Mk_annot :t: diff --git a/update_isla_lang.sh b/update_isla_lang.sh index ade1512..1f8a8d7 100755 --- a/update_isla_lang.sh +++ b/update_isla_lang.sh @@ -4,7 +4,7 @@ # the repository. Note that the script is self-modifying: it will change the # old hash into the new one, and erase the new hash again. -OLD_HASH=4ee3daa3a9f04b2d6a55dd94026ff5f9d79db5fc +OLD_HASH=309be26729b511570e2d31f69c6ba1ce1dc00779 NEW_HASH= sed -i "s/${OLD_HASH}/${NEW_HASH}/g" README.md .gitlab-ci.yml .github/workflows/ci.yml update_isla_lang.sh Makefile