Replace SailTinyArm by SailArm (Not to be merged)

.github/workflows/ci.yml

@@ -79,7 +79,7 @@ jobs:
         eval $(opam env)
         opam install --deps-only --confirm-level=unsafe-yes .
         # This is needed with opam 2.1, not with opam 2.3. I haven't tested 2.2
-        opam install --yes sail coq-sail-tiny-arm coq-sail-riscv
+        opam install --yes sail coq-sail-arm coq-sail-riscv
         opam clean
         opam clean -r
 

ArchSemArm/ArmInst.v

@@ -44,9 +44,9 @@
 
 Require Export SailStdpp.Base.
 Require Export SailStdpp.ConcurrencyInterfaceTypes.
-From ASCommon Require Import Options Common Effects.
+From ASCommon Require Import Options Common Effects FMon.
 
-Require Export SailTinyArm.System_types.
+Require Export SailArm.armv9_types.
 From ArchSem Require Import
   Interface FromSail TermModels CandidateExecutions GenPromising SeqModel.
 
@@ -62,14 +62,14 @@ Instance pretty_greg : Pretty greg :=
 
 (** First we import the sail generated interface modules *)
 Module Arm.
-  Module SA := System_types.Arch.
-  Module SI := System_types.Interface.
+  Module SA := armv9_types.Arch.
+  Module SI := armv9_types.Interface.
 
   (** Then we need to create a few new things for ArchSem *)
   Module ArchExtra <: FromSail.ArchExtra SA.
     Import SA.
 
-    Definition pc_reg : greg := GReg _PC.
+    Definition pc_reg : greg := GReg PC.
     Definition pretty_greg : Pretty greg := _.
   End ArchExtra.
 
@@ -107,7 +107,6 @@ Export ArmSeqModel.
 (** Make type abbreviations transparent *)
 #[export] Typeclasses Transparent bits.
 #[export] Typeclasses Transparent SA.addr_size.
-#[export] Typeclasses Transparent System_types.addr_space.
 #[export] Typeclasses Transparent SA.addr_space.
 #[export] Typeclasses Transparent SA.sys_reg_id.
 #[export] Typeclasses Transparent SA.mem_acc.
@@ -128,9 +127,10 @@ Export ArmSeqModel.
   Countable_register_values
   : typeclass_instances.
 
-Require SailTinyArm.System.
+Require SailArm.armv9.
 
-(** The semantics of instructions from system [sail-tiny-arm] by using the
-    conversion code from [ArchSem.FromSail] *)
-Definition sail_tiny_arm_sem (nondet : bool) : iMon () :=
-  iMon_from_Sail nondet (System.fetch_and_execute ()).
+(** The semantics of instructions from [sail-arm] by using the conversion code
+    from [ArchSem.FromSail]. [SEE] need to be reset manually between
+    instructions for legacy boring reasons *)
+Definition sail_arm_sem (nondet : bool) : iMon () :=
+  iMon_from_Sail nondet (armv9.__InstructionExecute ());; mcall (RegWrite SEE None 0).

ArchSemArm/VMSA22Arm.v

@@ -48,7 +48,7 @@ Require Import ASCommon.GRel.
 Require Import ASCommon.FMon.
 Require Import ArmInst.
 Require Import GenAxiomaticArm.
-Require Import SailTinyArm.System_types.
+Require Import SailArm.armv9_types.
 
 Import Candidate.
 

ArchSemArm/dune

@@ -4,14 +4,14 @@
  (modules
    ArmInst
    UMPromising
-   VMPromising
+   ; VMPromising
    GenAxiomaticArm
    UMArm
    UMSeqArm
    VMSA22Arm
    VMUMEquivThm
  )
- (theories stdpp Hammer RecordUpdate Equations Ltac2 SailStdpp ASCommon ArchSem SailTinyArm)
+ (theories stdpp Hammer RecordUpdate Equations Ltac2 SailStdpp ASCommon ArchSem SailArm)
  (coqdoc_flags :standard --utf8
                --external https://plv.mpi-sws.org/coqdoc/stdpp stdpp
                --external ../../Common/ASCommon.html ASCommon

ArchSemArm/tests/ArmSeqModelIslaTest.v

@@ -0,0 +1,67 @@
+From ASCommon Require Import Options Common.
+From ArchSemArm Require Import ArmInst IslaInit.
+From ASCommon Require Import CResult.
+
+
+Open Scope stdpp.
+Open Scope bv.
+
+(** Extract R0 in a Z on success to have something printable by Coq *)
+Definition r0_extract (a : Model.Res.t ∅ 1) : result string Z :=
+  match a with
+  | Model.Res.FinalState fs =>
+      let regs : registerMap := fs.(MState.regs) !!! 0%fin in
+      if reg_lookup R0 regs is Some r0
+      then Ok (bv_unsigned r0)
+      else Error "R0 not in state"
+  | Model.Res.Error s => Error s
+  | Model.Res.Unspecified e => match e with end
+  end.
+
+Definition regs_extract (a : Model.Res.t ∅ 1) : result string (list (sigT reg_type)) :=
+  match a with
+  | Model.Res.FinalState fs =>
+      let regs : registerMap := fs.(MState.regs) !!! 0%fin in
+      Ok (dmap_to_list regs)
+  | Model.Res.Error s => Error s
+  | Model.Res.Unspecified e => match e with end
+  end.
+
+(** Common configuration from Isla config files to run at EL0 in AArch64 mode *)
+Definition add_common_regs pre :=
+  pre
+  |> reg_insert PCUpdated false
+  |> reg_insert SPESampleInFlight false
+  |> reg_insert InGuardedPage false
+  |> reg_insert __supported_pa_size 52%Z
+  |> reg_insert SEE 0x0%Z
+.
+
+(** We test against the sail-arm semantic, with non-determinism disabled *)
+Definition arm_sem := sail_arm_sem false.
+
+Module STRLDR. (* STR X2, [X1, X0]; LDR X0, [X1, X0] with address in x1, zero in x0 *)
+  Definition init_reg : registerMap :=
+    nth 0 isla_threads_init_regs dmap_empty
+    |> add_common_regs.
+
+  Definition init_mem : memoryMap:=
+    isla_init_mem.
+
+  Definition termCond : terminationCondition 1 :=
+    (λ tid rm, reg_lookup PC rm =? Some (0x400008 : bv 64)).
+
+  Definition initState :=
+    {|MState.state :=
+        {|MState.memory := init_mem;
+          MState.regs := [# init_reg];
+          MState.address_space := PAS_NonSecure |};
+      MState.termCond := termCond |}.
+  Definition test_results := sequential_modelc None 2 arm_sem 1%nat initState.
+
+  Goal r0_extract <$> test_results = Listset [Ok 0x2a%Z].
+    vm_compute (_ <$> _).
+    reflexivity.
+  Qed.
+End STRLDR.
+

ArchSemArm/tests/ArmSeqModelTest.v

@@ -63,26 +63,92 @@ Definition r0_extract (a : Model.Res.t ∅ 1) : result string Z :=
   | Model.Res.Unspecified e => match e with end
   end.
 
-(** We test against the sail-tiny-arm semantic, with non-determinism enabled *)
-Definition arm_sem := sail_tiny_arm_sem true.
+Definition regs_extract (a : Model.Res.t ∅ 1) : result string (list (sigT reg_type)) :=
+  match a with
+  | Model.Res.FinalState fs =>
+      let regs : registerMap := fs.(MState.regs) !!! 0%fin in
+      Ok (dmap_to_list regs)
+  | Model.Res.Error s => Error s
+  | Model.Res.Unspecified e => match e with end
+  end.
+
+Fixpoint FeatureImpl_from_features (l : list Feature) : vec bool 259 :=
+  match l with
+  | [] => vector_init 259%Z false
+  | x :: tl => vec_update_dec (FeatureImpl_from_features tl) (num_of_Feature x) true
+  end.
 
+(** Common configuration from Isla config files to run at EL0 in AArch64 mode *)
+Definition common_init_regs :=
+  ∅
+  |> reg_insert _PC 0x0
+  |> reg_insert PCUpdated false
+  |> reg_insert _EDSCR 0x0
+  |> reg_insert MDCCSR_EL0 0x0
+  |> reg_insert EDESR 0x0
+  |> reg_insert PSTATE inhabitant
+  |> reg_insert ShouldAdvanceIT false
+  |> reg_insert ShouldAdvanceSS false
+  |> reg_insert FeatureImpl $
+       FeatureImpl_from_features [FEAT_AA64EL0; FEAT_EL0]
+  (* Bit 1 is NS for Non-Secure mode below EL3
+     Bit 10 is RW for AArch64 mode below EL3 *)
+  |> reg_insert SCR_EL3 0x401
+  |> reg_insert _MPAM3_EL3 0x0
+  |> reg_insert MPAM2_EL2 0x0
+  |> reg_insert BTypeCompatible false
+  |> reg_insert MDCR_EL2 0x0
+  |> reg_insert HCR_EL2 0x0000000080000000 (* rw flag, AArch64 below EL2 *)
+  |> reg_insert OSLSR_EL1 0x0
+  |> reg_insert __InstructionStep false
+  |> reg_insert SPESampleInFlight false
+  |> reg_insert _VTTBR_EL2 0x0
+  |> reg_insert VTTBR 0x0
+  |> reg_insert TCR_EL1 0x0
+  |> reg_insert _TTBR0_EL1 0x0
+  |> reg_insert TTBR0_NS 0x0
+  (* Bit 1 being unset allows unaligned accesses
+     Bit 9 being set allows DAIF bits to be set at EL0
+     Bit 26 being set allows cache-maintenance ops in EL0 *)
+  |> reg_insert SCTLR_EL1 0x0000000004000200
+  |> reg_insert MAIR_EL1 0x0
+  |> reg_insert InGuardedPage false
+  |> reg_insert __supported_pa_size 52%Z
+  |> reg_insert VTCR_EL2 0x0
+  |> reg_insert SCTLR_EL2 0x0
+  |> reg_insert __emulator_termination_opcode None
+  |> reg_insert PMCR_EL0 0x0
+  |> reg_insert __BranchTaken false
+  |> reg_insert __ExclusiveMonitorSet false
+  |> reg_insert __ThisInstrEnc inhabitant
+  |> reg_insert __ThisInstr 0x0
+  |> reg_insert __currentCond 0x0
+  |> reg_insert SEE 0x0%Z
+  |> reg_insert BTypeNext 0x0
+  |> reg_insert MDSCR_EL1 0x0
+  |> reg_insert Branchtypetaken inhabitant.
+
+(** We test against the sail-arm semantic, with non-determinism disabled *)
+Definition arm_sem := sail_arm_sem false.
 
 (* Run EOR X0, X1, X2 at pc address 0x500, whose opcode is 0xca020020 *)
 Module EOR.
 
 Definition init_reg : registerMap :=
-  ∅
-  |> reg_insert _PC 0x500
+  common_init_regs
+  |> reg_insert PC 0x500
   |> reg_insert R0 0x0
   |> reg_insert R1 0x11
-  |> reg_insert R2 0x101.
+  |> reg_insert R2 0x101
+ .
 
 Definition init_mem : memoryMap:=
   ∅
-  |> mem_insert 0x500 4 0xca020020. (* EOR X0, X1, X2 *)
+  |> mem_insert 0x500 4 0xca020020 (* EOR X0, X1, X2 *)
+  |> mem_insert 0x504 4 0xca020020. (* EOR X0, X1, X2 *)
 
 Definition termCond : terminationCondition 1 :=
-  (λ tid rm, reg_lookup _PC rm =? Some (0x504 : bv 64)).
+  (λ tid rm, reg_lookup PC rm =? Some (0x504 : bv 64)).
 
 Definition initState :=
   {|MState.state :=
@@ -101,8 +167,8 @@ End EOR.
 
 Module LDR. (* LDR X0, [X1, X0] at 0x500, loading from 0x1000 *)
 Definition init_reg : registerMap :=
-  ∅
-  |> reg_insert _PC 0x500
+  common_init_regs
+  |> reg_insert PC 0x500
   |> reg_insert R0 0x1000
   |> reg_insert R1 0x0.
 
@@ -112,7 +178,7 @@ Definition init_mem : memoryMap:=
   |> mem_insert 0x1000 8 0x2a. (* data to be read *)
 
 Definition termCond : terminationCondition 1 :=
-  (λ tid rm, reg_lookup _PC rm =? Some (0x504 : bv 64)).
+  (λ tid rm, reg_lookup PC rm =? Some (0x504 : bv 64)).
 
 Definition initState :=
   {|MState.state :=
@@ -130,8 +196,8 @@ End LDR.
 
 Module STRLDR. (* STR X2, [X1, X0]; LDR X0, [X1, X0] at 0x500, using address 0x1100 *)
   Definition init_reg : registerMap :=
-    ∅
-    |> reg_insert _PC 0x500
+    common_init_regs
+    |> reg_insert PC 0x500
     |> reg_insert R0 0x1000
     |> reg_insert R1 0x100
     |> reg_insert R2 0x2a.
@@ -143,7 +209,7 @@ Module STRLDR. (* STR X2, [X1, X0]; LDR X0, [X1, X0] at 0x500, using address 0x1
     |> mem_insert 0x1100 8 0x0. (* Memory need to exists to be written to *)
 
   Definition termCond : terminationCondition 1 :=
-    (λ tid rm, reg_lookup _PC rm =? Some (0x508 : bv 64)).
+    (λ tid rm, reg_lookup PC rm =? Some (0x508 : bv 64)).
 
   Definition initState :=
     {|MState.state :=
@@ -158,3 +224,38 @@ Module STRLDR. (* STR X2, [X1, X0]; LDR X0, [X1, X0] at 0x500, using address 0x1
     reflexivity.
   Qed.
 End STRLDR.
+
+Module Factorial. (* https://godbolt.org/z/rEfMMo5Tv *)
+  Definition init_reg : registerMap :=
+    common_init_regs
+    |> reg_insert PC 0x500
+    |> reg_insert R0 5
+    |> reg_insert R1 0
+    |> reg_insert R30 0x1234.
+
+  Definition init_mem : memoryMap:=
+    ∅
+    |> mem_insert 0x500 4 0x2a0003e1  (* MOV  W1, W0 *)
+    |> mem_insert 0x504 4 0x52800020  (* MOVZ X0, 0x1 *)
+    |> mem_insert 0x508 4 0x34000081  (* CBZ  W1, 0x518 (PC relative) *)
+    |> mem_insert 0x50c 4 0x1b017c00  (* MUL W0, W0, W1 *)
+    |> mem_insert 0x510 4 0x71000421  (* SUBS W1, W1, 1 *)
+    |> mem_insert 0x514 4 0x54ffffc1  (* B.NE 0x50c (PC relative) *)
+    |> mem_insert 0x518 4 0xD65F03C0. (* RET *)
+
+  Definition termCond : terminationCondition 1 :=
+    (λ tid rm, reg_lookup PC rm =? Some (0x1234 : bv 64)).
+
+  Definition initState :=
+    {|MState.state :=
+        {|MState.memory := init_mem;
+          MState.regs := [# init_reg];
+          MState.address_space := PAS_NonSecure |};
+      MState.termCond := termCond |}.
+  Definition test_results := sequential_modelc None 100 arm_sem 1%nat initState.
+
+  Goal r0_extract <$> test_results = Listset [Ok 120%Z].
+    vm_compute (_ <$> _).
+    reflexivity.
+  Qed.
+End Factorial.