Add SCTLR on the model and tests

Author: febyeji

ArchSemArm/VMPromising.v

@@ -413,7 +413,10 @@ Definition relaxed_regs : gset reg :=
       GReg MMFR0_EL1;
       GReg MMFR1_EL1;
       GReg MMFR2_EL1;
-      GReg MMFR3_EL1].
+      GReg MMFR3_EL1;
+      GReg SCTLR_EL1;
+      GReg SCTLR_EL2;
+      GReg SCTLR_EL3].
 
 (** Determine if input register is an unknown register from the architecture *)
 Definition is_reg_unknown (r : reg) : Prop :=

ArchSemArm/tests/ArmSeqModelTest.v

@@ -75,7 +75,8 @@ Definition init_reg : registerMap :=
   |> reg_insert _PC 0x500
   |> reg_insert R0 0x0
   |> reg_insert R1 0x11
-  |> reg_insert R2 0x101.
+  |> reg_insert R2 0x101
+  |> reg_insert SCTLR_EL1 0x0.
 
 Definition init_mem : memoryMap:=
   ∅
@@ -104,7 +105,8 @@ Definition init_reg : registerMap :=
   ∅
   |> reg_insert _PC 0x500
   |> reg_insert R0 0x1000
-  |> reg_insert R1 0x0.
+  |> reg_insert R1 0x0
+  |> reg_insert SCTLR_EL1 0x0.
 
 Definition init_mem : memoryMap:=
   ∅
@@ -134,7 +136,8 @@ Module STRLDR. (* STR X2, [X1, X0]; LDR X0, [X1, X0] at 0x500, using address 0x1
     |> reg_insert _PC 0x500
     |> reg_insert R0 0x1000
     |> reg_insert R1 0x100
-    |> reg_insert R2 0x2a.
+    |> reg_insert R2 0x2a
+    |> reg_insert SCTLR_EL1 0x0.
 
   Definition init_mem : memoryMap:=
     ∅

ArchSemArm/tests/UMPromisingTest.v

@@ -92,7 +92,8 @@ Module EOR.
     |> reg_insert _PC 0x500
     |> reg_insert R0 0x0
     |> reg_insert R1 0x11
-    |> reg_insert R2 0x101.
+    |> reg_insert R2 0x101
+    |> reg_insert SCTLR_EL1 0x0.
 
   Definition init_mem : memoryMap :=
     ∅
@@ -125,7 +126,8 @@ Module LDR. (* LDR X0, [X1, X0] at 0x500, loading from 0x1000 *)
     ∅
     |> reg_insert _PC 0x500
     |> reg_insert R0 0x1000
-    |> reg_insert R1 0x0.
+    |> reg_insert R1 0x0
+    |> reg_insert SCTLR_EL1 0x0.
 
   Definition init_mem : memoryMap:=
     ∅
@@ -160,7 +162,8 @@ Module STRLDR. (* STR X2, [X1, X0]; LDR X0, [X1, X0] at 0x500, using address 0x1
     |> reg_insert _PC 0x500
     |> reg_insert R0 0x1000
     |> reg_insert R1 0x100
-    |> reg_insert R2 0x2a.
+    |> reg_insert R2 0x2a
+    |> reg_insert SCTLR_EL1 0x0.
 
   Definition init_mem : memoryMap:=
     ∅
@@ -205,7 +208,8 @@ Module MP.
     |> reg_insert R3 0x1000
     |> reg_insert R4 0x200
     |> reg_insert R2 0x2a
-    |> reg_insert R5 0x1.
+    |> reg_insert R5 0x1
+    |> reg_insert SCTLR_EL1 0x0.
 
   Definition init_reg_t2 : registerMap :=
     ∅
@@ -215,7 +219,8 @@ Module MP.
     |> reg_insert R3 0x1000
     |> reg_insert R4 0x200
     |> reg_insert R2 0x0
-    |> reg_insert R5 0x0.
+    |> reg_insert R5 0x0
+    |> reg_insert SCTLR_EL1 0x0.
 
   Definition init_mem : memoryMap :=
     ∅
@@ -272,7 +277,8 @@ Module MPDMBS.
     |> reg_insert R3 0x1000
     |> reg_insert R4 0x200
     |> reg_insert R2 0x2a
-    |> reg_insert R5 0x1.
+    |> reg_insert R5 0x1
+    |> reg_insert SCTLR_EL1 0x0.
 
   Definition init_reg_t2 : registerMap :=
     ∅
@@ -282,7 +288,8 @@ Module MPDMBS.
     |> reg_insert R3 0x1000
     |> reg_insert R4 0x200
     |> reg_insert R2 0x0
-    |> reg_insert R5 0x0.
+    |> reg_insert R5 0x0
+    |> reg_insert SCTLR_EL1 0x0.
 
   Definition init_mem : memoryMap :=
     ∅

coq-archsem-arm.opam

@@ -38,7 +38,7 @@ build: [
 ]
 dev-repo: "git+https://github.com/rems-project/archsem.git"
 pin-depends: [
-  [ "coq-sail-tiny-arm.dev" "git+https://github.com/rems-project/sail-tiny-arm.git#df3a676"]
+  [ "coq-sail-tiny-arm.dev" "git+https://github.com/rems-project/sail-tiny-arm.git#aff39e1"]
   [ "libsail.0.19.1" "git+https://github.com/rems-project/sail.git#54574467"]
   [ "sail.0.19.1" "git+https://github.com/rems-project/sail.git#54574467"]
   [ "sail_c_backend.0.19.1" "git+https://github.com/rems-project/sail.git#54574467"]

coq-archsem-arm.opam.template

@@ -1,5 +1,5 @@
 pin-depends: [
-  [ "coq-sail-tiny-arm.dev" "git+https://github.com/rems-project/sail-tiny-arm.git#df3a676"]
+  [ "coq-sail-tiny-arm.dev" "git+https://github.com/rems-project/sail-tiny-arm.git#aff39e1"]
   [ "libsail.0.19.1" "git+https://github.com/rems-project/sail.git#54574467"]
   [ "sail.0.19.1" "git+https://github.com/rems-project/sail.git#54574467"]
   [ "sail_c_backend.0.19.1" "git+https://github.com/rems-project/sail.git#54574467"]