Library ArchSemRiscV.RiscVInst

From SailStdpp Require Import -(notations) Base ConcurrencyInterfaceTypes.

From Riscv Require Export rv64d_types.
From Riscv Require Import rv64d.

From ASCommon Require Import Options.
From ASCommon Require Import Common FMon.

From ArchSem Require Import
Interface TermModels CandidateExecutions GenPromising SeqModel ArchInst.
From ArchSem Require Export FromSail.

Module SA := rv64d_types.Arch.
Module SI := rv64d_types.Interface.

There a few missing definition that are not generated by Sail

Module ArchExtra <: FromSail.ArchExtra SA.
  Import SA.

  Definition pc_reg : reg := PC.
  Definition reg_of_string := register_of_string.

  Equations reg_type_of_gen (r : reg) (rv : reg_gen_val) :
    result string (reg_type r) :=
    reg_type_of_gen (R_bitvector_1 _) (RVNumber z) := Ok (Z_to_bv 1 z);
    reg_type_of_gen (R_bitvector_3 _) (RVNumber z) := Ok (Z_to_bv 3 z);
    reg_type_of_gen (R_bitvector_4 _) (RVNumber z) := Ok (Z_to_bv 4 z);
    reg_type_of_gen (R_bitvector_5 _) (RVNumber z) := Ok (Z_to_bv 5 z);
    reg_type_of_gen (R_bitvector_32 _) (RVNumber z) := Ok (Z_to_bv 32 z);
    reg_type_of_gen (R_bitvector_64 _) (RVNumber z) := Ok (Z_to_bv 64 z);
    reg_type_of_gen (R_bitvector_128 _) (RVNumber z) := Ok (Z_to_bv 128 z);
    reg_type_of_gen (R_bitvector_192 _) (RVNumber z) := Ok (Z_to_bv 192 z);
    reg_type_of_gen (R_bitvector_320 _) (RVNumber z) := Ok (Z_to_bv 320 z);
    reg_type_of_gen r _ := Error ("error decoding " ++ pretty r)%string.

  Equations reg_type_to_gen (r : reg) (rv : reg_type r) : reg_gen_val :=
    reg_type_to_gen (R_bitvector_1 _) bv := RVNumber (bv_unsigned bv);
    reg_type_to_gen (R_bitvector_3 _) bv := RVNumber (bv_unsigned bv);
    reg_type_to_gen (R_bitvector_4 _) bv := RVNumber (bv_unsigned bv);
    reg_type_to_gen (R_bitvector_5 _) bv := RVNumber (bv_unsigned bv);
    reg_type_to_gen (R_bitvector_32 _) bv := RVNumber (bv_unsigned bv);
    reg_type_to_gen (R_bitvector_64 _) bv := RVNumber (bv_unsigned bv);
    reg_type_to_gen (R_bitvector_128 _) bv := RVNumber (bv_unsigned bv);
    reg_type_to_gen (R_bitvector_192 _) bv := RVNumber (bv_unsigned bv);
    reg_type_to_gen (R_bitvector_320 _) bv := RVNumber (bv_unsigned bv);
    reg_type_to_gen r _ := RVString ("error encoding " ++ pretty r).

End ArchExtra.

Then we can use this to generate an ArchSem architecture module

Module Arch := ArchFromSail SA ArchExtra.

Module NoCHERI.
Definition no_cheri : ¬ Arch.CHERI := ltac:(naive_solver).
End NoCHERI.

This instantiates all ArchSem arch-generic code, for RiscV

Module RiscV := ArchInst.ArchInst Arch NoCHERI.

Module IMonFromSail := IMonFromSail SA SI ArchExtra Arch RiscV.Interface.

Export Arch.
Export RiscV.
Export RiscV.Interface.
Export RiscV.TM.
Export RiscV.Cand.
Export RiscV.GenPro.
Export RiscV.SeqModel.
Export RiscV.ISAManip.
Export IMonFromSail.

Make type abbreviations transparent

#[export] Typeclasses Transparent bits.
#[export] Typeclasses Transparent SA.addr_size.
#[export] Typeclasses Transparent SA.addr_space.
#[export] Typeclasses Transparent SA.sys_reg_id.
#[export] Typeclasses Transparent SA.mem_acc.
#[export] Typeclasses Transparent SA.abort.
#[export] Typeclasses Transparent SA.barrier.
#[export] Typeclasses Transparent SA.cache_op.
#[export] Typeclasses Transparent SA.tlbi.
#[export] Typeclasses Transparent SA.exn.
#[export] Typeclasses Transparent SA.trans_start.
#[export] Typeclasses Transparent SA.trans_end.

Since ArchSem only uses register types through reg_type, there is no need for those slow and risky instances

#[export] Remove Hints
  Decidable_eq_register_values
  Inhabited_register_values
  Countable_register_values
  : typeclass_instances.

The semantics of instructions from sail-riscv by using the conversion code from ArchSem.FromSail.

Definition sail_riscv_sem (nondet : bool) : iMon () :=
iMon_from_Sail nondet (rv64d.try_step 0 true);; mret ().