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
 

ArchSem/FromSail.v

@@ -92,46 +92,44 @@ an architecture instantiation that is missing from the Sail generated code *)
 Module Type ArchExtra (SA : SailArch).
   Import SA.
 
-  Parameter pc_reg : greg.
-  Parameter pretty_greg : Pretty greg.
+  Parameter pc_reg : reg.
 End ArchExtra.
 
 (** * Convert from Sail generated instantiations to ArchSem ones *)
 
 Module ArchFromSail (SA : SailArch) (AE : ArchExtra SA) <: Arch.
   Import (hints) SA.
-  Definition reg := SA.greg.
+  Definition reg := SA.reg.
   #[export] Typeclasses Transparent reg.
-  Definition reg_eq : EqDecision reg := SA.greg_eq.
+  Definition reg_eq : EqDecision reg := SA.reg_eq.
   #[export] Typeclasses Transparent reg_eq.
-  Definition reg_countable : Countable reg := SA.greg_cnt.
-  #[export] Typeclasses Transparent reg_countable.
-  Definition pretty_reg : Pretty reg := AE.pretty_greg.
+  Definition reg_countable : Countable reg := SA.reg_countable.
   #[export] Typeclasses Transparent reg_countable.
+  Definition pretty_reg : Pretty reg := SA.reg_pretty.
+  #[export] Typeclasses Transparent pretty_reg.
 
 
   Definition pc_reg := AE.pc_reg.
   #[export] Typeclasses Transparent pc_reg.
 
-  Definition reg_type (r : reg) := match r with @SA.GReg A _ => A end.
-  #[export] Instance reg_type_eq (r : reg) : EqDecision (reg_type r).
-  Proof. destruct r. by apply SA.regval_eq. Defined.
-  #[export] Instance reg_type_countable (r : reg) : Countable (reg_type r).
-  Proof. destruct r. by apply SA.regval_cnt. Defined.
-  #[export] Instance reg_type_inhabited (r : reg) : Inhabited (reg_type r).
-  Proof. destruct r. by apply SA.regval_inhabited. Defined.
+  Definition reg_type := SA.reg_type.
+  #[export] Typeclasses Transparent reg_type.
+  #[export] Instance reg_type_eq (r : reg) : EqDecision (reg_type r) := SA.reg_type_eq r.
+  #[export] Instance reg_type_countable (r : reg) : Countable (reg_type r) := SA.reg_type_countable r.
+  #[export] Instance reg_type_inhabited (r : reg) : Inhabited (reg_type r) := SA.reg_type_inhabited r.
   #[export] Instance ctrans_reg_type : CTrans reg_type.
   Proof.
-    intros [Tx x] [Ty y] e a. cbn in *.
+    intros x y e a.
     by eapply SA.regval_transport.
   Defined.
   #[export] Instance ctrans_reg_type_simpl : CTransSimpl reg_type.
-  Proof. intros [Tx x] e a. apply SA.regval_transport_sound. Qed.
+  Proof. intros x e a. apply SA.regval_transport_sound. Qed.
   #[export] Instance reg_type_eq_dep_dec : EqDepDecision reg_type.
   Proof.
-    intros [Tx x] [Ty y] e a b.
-    refine (dec_if (decide (ctrans e a = b)));
-      abstract (dependent destruction e; simp ctrans in *; by rewrite JMeq_simpl).
+    intros x y e a b.
+    subst x.
+    rewrite JMeq_simpl.
+    by apply reg_type_eq.
   Defined.
 
   (* TODO get sail to generate reg_acc *)
@@ -218,28 +216,12 @@ Module IMonFromSail (SA : SailArch) (SI : SailInterfaceT SA)
   Import I.
   Import (coercions) SA.
 
-  Definition MemReq_from_sail_read {n nt} (rr : SI.ReadReq.t n nt) : MemReq.t :=
-    {|MemReq.address := rr.(SI.ReadReq.address);
-      MemReq.access_kind := rr.(SI.ReadReq.access_kind);
-      MemReq.address_space := rr.(SI.ReadReq.address_space);
-      MemReq.size := n;
-      MemReq.num_tag := nt;
-    |}.
-
-  Definition MemReq_from_sail_announce {n nt} (rr : SI.AddressAnnounce.t n nt) : MemReq.t :=
-    {|MemReq.address := rr.(SI.AddressAnnounce.address);
-      MemReq.access_kind := rr.(SI.AddressAnnounce.access_kind);
-      MemReq.address_space := rr.(SI.AddressAnnounce.address_space);
-      MemReq.size := n;
-      MemReq.num_tag := nt;
-    |}.
-
-  Definition MemReq_from_sail_write {n nt} (rr : SI.WriteReq.t n nt) : MemReq.t :=
-    {|MemReq.address := rr.(SI.WriteReq.address);
-      MemReq.access_kind := rr.(SI.WriteReq.access_kind);
-      MemReq.address_space := rr.(SI.WriteReq.address_space);
-      MemReq.size := n;
-      MemReq.num_tag := nt;
+  Definition MemReq_from_sail (rr : SI.MemReq.t) : MemReq.t :=
+    {|MemReq.address := rr.(SI.MemReq.address);
+      MemReq.access_kind := rr.(SI.MemReq.access_kind);
+      MemReq.address_space := rr.(SI.MemReq.address_space);
+      MemReq.size := rr.(SI.MemReq.size);
+      MemReq.num_tag := rr.(SI.MemReq.num_tag);
     |}.
 
   Definition Sail_choose (ct : ChooseType) : I.iMon (choose_type ct) :=
@@ -272,21 +254,21 @@ Module IMonFromSail (SA : SailArch) (SI : SailInterfaceT SA)
     match out with
     | SI.RegRead reg acc => mcall (RegRead reg acc)
     | SI.RegWrite reg acc regval => mcall (RegWrite reg acc regval)
-    | SI.MemRead n nt rr =>
-        mcall (MemRead (MemReq_from_sail_read rr))
+    | SI.MemRead rr =>
+        mcall (MemRead (MemReq_from_sail rr))
           |$> (λ o, match o with
                     | Ok (val, tags) => inl (val, tags)
                     | Error a => inr a
                     end)
-    | SI.MemWrite n nt wr =>
-        mcall (MemWrite (MemReq_from_sail_write wr)
-                 wr.(SI.WriteReq.value) wr.(SI.WriteReq.tags))
+    | SI.MemWrite wr value tags =>
+        mcall (MemWrite (MemReq_from_sail wr)
+                 value tags)
           |$> (λ o, match o with
                     | Ok () => inl (Some true)
                     | Error a => inr a
                     end)
-    | SI.MemAddressAnnounce n nt aa =>
-        mcall (MemWriteAddrAnnounce (MemReq_from_sail_announce aa))
+    | SI.MemAddressAnnounce aa =>
+        mcall (MemWriteAddrAnnounce (MemReq_from_sail aa))
     | SI.InstrAnnounce _ => mret ()
     | SI.BranchAnnounce _ _ => mret ()
     | SI.Barrier b => mcall (Barrier b)

ArchSemArm/ArmInst.v

@@ -44,33 +44,25 @@
 
 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.
 
 Open Scope stdpp.
 
 
-(** Export [GReg] definitions and typeclasses, since it's what we will
-    manipulate for registers *)
-Export GRegister.
-Coercion GReg : register >-> greg.
-Instance pretty_greg : Pretty greg :=
-  λ '(GReg reg), string_of_register reg.
-
 (** 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 pretty_greg : Pretty greg := _.
+    Definition pc_reg : reg := PC.
   End ArchExtra.
 
   (** Then we can use this to generate an ArchSem architecture module *)
@@ -107,7 +99,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 +119,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.
+