fix pinning of isla-lang

rems-project · Dec 13, 2023 · 608a69e · 608a69e
1 parent e2b84be
commit 608a69e
Show file tree

Hide file tree

Showing 12 changed files with 14 additions and 18 deletions.
diff --git 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,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://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
 
 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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